Patchwork [Ada] Disabled invariants and preconditions and _Postconditions

login
register
mail settings
Submitter Arnaud Charlet
Date April 24, 2013, 2:56 p.m.
Message ID <20130424145657.GA1080@adacore.com>
Download mbox | patch
Permalink /patch/239222/
State New
Headers show

Comments

Arnaud Charlet - April 24, 2013, 2:56 p.m.
This patch disables the generation of internal procedure _Postconditions when
invariants and preconditions are disabled.

------------
-- Source --
------------

--  main.adb

procedure Main is
   X : Integer := 0;
   type R is new Integer with Predicate => X > 0;
   package Pack is
      type T is tagged private;
      procedure P (Arg1 : in out T; Arg2 : in out R) with
        Post       => X > 0,
        Post'Class => X > 0;
   private
      type T is tagged null record with Invariant => X > 0;
   end Pack;
   package body Pack is
      procedure P (Arg1 : in out T; Arg2 : in out R) is
      begin
         null;
      end P;
   end Pack;
   use Pack;
   Y : T;
   Z : R := 2;
begin
   P (Y, Z);
end Main;

-----------------
-- Compilation --
-----------------

$ gcc -c -gnat12 -gnatd.V -gnatDG main.adb
$ grep "postconditions" main.adb.dg

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

2013-04-24  Hristian Kirtchev  <kirtchev@adacore.com>

	* exp_ch6.adb (Expand_Actuals): Add a predicate check on an
	actual the related type has a predicate function.
	* sem_ch3.adb (Constant_Redeclaration): Ensure that the related
	type has an invariant procedure before building a call to it.
	* sem_ch6.adb (Append_Enabled_Item): New routine.
	(Check_Access_Invariants): Use routine
	Append_Enabled_Item to chain onto the list of postconditions.
	(Contains_Enabled_Pragmas): Removed.
	(Expand_Contract_Cases): Use routine Append_Enabled_Item to chain onto
	the list of postconditions.
	(Invariants_Or_Predicates_Present): Removed.
	(Process_PPCs): Partially reimplemented.

Patch

Index: sem_ch3.adb
===================================================================
--- sem_ch3.adb	(revision 198241)
+++ sem_ch3.adb	(working copy)
@@ -10761,13 +10761,9 @@ 
          --  A deferred constant is a visible entity. If type has invariants,
          --  verify that the initial value satisfies them.
 
-         if Expander_Active and then Has_Invariants (T) then
-            declare
-               Call : constant Node_Id :=
-                 Make_Invariant_Call (New_Occurrence_Of (Prev, Sloc (N)));
-            begin
-               Insert_After (N, Call);
-            end;
+         if Has_Invariants (T) and then Present (Invariant_Procedure (T)) then
+            Insert_After (N,
+              Make_Invariant_Call (New_Occurrence_Of (Prev, Sloc (N))));
          end if;
       end if;
    end Constant_Redeclaration;
Index: exp_ch6.adb
===================================================================
--- exp_ch6.adb	(revision 198234)
+++ exp_ch6.adb	(working copy)
@@ -1728,17 +1728,19 @@ 
             --  procedure does not include a predicate call, so it has to be
             --  generated explicitly.
 
-            if (Has_Aspect (E_Actual, Aspect_Predicate)
-                  or else
-                Has_Aspect (E_Actual, Aspect_Dynamic_Predicate)
-                  or else
-                Has_Aspect (E_Actual, Aspect_Static_Predicate))
-              and then not Is_Init_Proc (Subp)
+            if not Is_Init_Proc (Subp)
+              and then (Has_Aspect (E_Actual, Aspect_Predicate)
+                          or else
+                        Has_Aspect (E_Actual, Aspect_Dynamic_Predicate)
+                          or else
+                        Has_Aspect (E_Actual, Aspect_Static_Predicate))
+              and then Present (Predicate_Function (E_Actual))
             then
-               if (Is_Derived_Type (E_Actual)
-                    and then Is_Overloadable (Subp)
-                    and then Is_Inherited_Operation_For_Type (Subp, E_Actual))
-                 or else Is_Entity_Name (Actual)
+               if Is_Entity_Name (Actual)
+                 or else
+                   (Is_Derived_Type (E_Actual)
+                     and then Is_Overloadable (Subp)
+                     and then Is_Inherited_Operation_For_Type (Subp, E_Actual))
                then
                   Append_To (Post_Call,
                     Make_Predicate_Check (E_Actual, Actual));
Index: sem_ch6.adb
===================================================================
--- sem_ch6.adb	(revision 198238)
+++ sem_ch6.adb	(working copy)
@@ -332,14 +332,14 @@ 
          end;
       end if;
 
-      Prev     := Current_Entity_In_Scope (Defining_Entity (Spec));
+      Prev := Current_Entity_In_Scope (Defining_Entity (Spec));
 
       --  If there are previous overloadable entities with the same name,
       --  check whether any of them is completed by the expression function.
 
       if Present (Prev) and then Is_Overloadable (Prev) then
-         Def_Id   := Analyze_Subprogram_Specification (Spec);
-         Prev     := Find_Corresponding_Spec (N);
+         Def_Id := Analyze_Subprogram_Specification (Spec);
+         Prev   := Find_Corresponding_Spec (N);
       end if;
 
       Ret := Make_Simple_Return_Statement (LocX, Expression (N));
@@ -11198,18 +11198,17 @@ 
       Plist : List_Id := No_List;
       --  List of generated postconditions
 
+      procedure Append_Enabled_Item (Item : Node_Id; List : in out List_Id);
+      --  Append a node to a list. If there is no list, create a new one. When
+      --  the item denotes a pragma, it is added to the list only when it is
+      --  enabled.
+
       procedure Check_Access_Invariants (E : Entity_Id);
       --  If the subprogram returns an access to a type with invariants, or
       --  has access parameters whose designated type has an invariant, then
       --  under the same visibility conditions as for other invariant checks,
       --  the type invariant must be applied to the returned value.
 
-      function Contains_Enabled_Pragmas (L : List_Id) return Boolean;
-      --  Determine whether list L has at least one enabled pragma. The routine
-      --  ignores other non-pragma elements.
-      --  This is NOT what the routine does??? It returns False if there is
-      --  one ignored pragma ???
-
       procedure Expand_Contract_Cases (CCs : Node_Id; Subp_Id : Entity_Id);
       --  Given pragma Contract_Cases CCs, create the circuitry needed to
       --  evaluate case guards and trigger consequence expressions. Subp_Id
@@ -11226,11 +11225,6 @@ 
       procedure Insert_After_Last_Declaration (Nod : Node_Id);
       --  Insert node Nod after the last declaration of the context
 
-      function Invariants_Or_Predicates_Present return Boolean;
-      --  Determines if any invariants or predicates are present for any OUT
-      --  or IN OUT parameters of the subprogram, or (for a function) if the
-      --  return value has an invariant.
-
       function Is_Public_Subprogram_For (T : Entity_Id) return Boolean;
       --  T is the entity for a private type for which invariants are defined.
       --  This function returns True if the procedure corresponding to the
@@ -11240,6 +11234,30 @@ 
       --  that an invariant check is required (for an IN OUT parameter, or
       --  the returned value of a function.
 
+      -------------------------
+      -- Append_Enabled_Item --
+      -------------------------
+
+      procedure Append_Enabled_Item (Item : Node_Id; List : in out List_Id) is
+      begin
+         --  Do not chain ignored or disabled pragmas
+
+         if Nkind (Item) = N_Pragma
+           and then (Is_Ignored (Item) or else Is_Disabled (Item))
+         then
+            null;
+
+         --  Add the item
+
+         else
+            if No (List) then
+               List := New_List;
+            end if;
+
+            Append (Item, List);
+         end if;
+      end Append_Enabled_Item;
+
       -----------------------------
       -- Check_Access_Invariants --
       -----------------------------
@@ -11266,39 +11284,18 @@ 
 
                Call := Make_Invariant_Call (Obj);
 
-               Append_To (Plist,
-                 Make_If_Statement (Loc,
-                   Condition =>
-                     Make_Op_Ne (Loc,
-                       Left_Opnd   => Make_Null (Loc),
-                       Right_Opnd  => New_Occurrence_Of (E, Loc)),
-                   Then_Statements => New_List (Call)));
+               Append_Enabled_Item
+                 (Make_If_Statement (Loc,
+                    Condition =>
+                      Make_Op_Ne (Loc,
+                        Left_Opnd   => Make_Null (Loc),
+                        Right_Opnd  => New_Occurrence_Of (E, Loc)),
+                    Then_Statements => New_List (Call)),
+                  List => Plist);
             end if;
          end if;
       end Check_Access_Invariants;
 
-      ------------------------------
-      -- Contains_Enabled_Pragmas --
-      ------------------------------
-
-      --  This routine does not implement its documented spec ???
-
-      function Contains_Enabled_Pragmas (L : List_Id) return Boolean is
-         Prag : Node_Id;
-
-      begin
-         Prag := First (L);
-         while Present (Prag) loop
-            if Nkind (Prag) = N_Pragma and then Is_Ignored (Prag) then
-               return False;
-            end if;
-
-            Next (Prag);
-         end loop;
-
-         return True;
-      end Contains_Enabled_Pragmas;
-
       ---------------------------
       -- Expand_Contract_Cases --
       ---------------------------
@@ -11759,11 +11756,7 @@ 
          --  Raise Assertion_Error when the corresponding consequence of a case
          --  guard that evaluated to True fails.
 
-         if No (Plist) then
-            Plist := New_List;
-         end if;
-
-         Append_To (Plist, Conseq_Checks);
+         Append_Enabled_Item (Conseq_Checks, Plist);
       end Expand_Contract_Cases;
 
       --------------
@@ -11889,51 +11882,6 @@ 
          end if;
       end Insert_After_Last_Declaration;
 
-      --------------------------------------
-      -- Invariants_Or_Predicates_Present --
-      --------------------------------------
-
-      function Invariants_Or_Predicates_Present return Boolean is
-         Formal : Entity_Id;
-
-      begin
-         --  Check function return result. If result is an access type there
-         --  may be invariants on the designated type.
-
-         if Ekind (Designator) /= E_Procedure
-           and then Has_Invariants (Etype (Designator))
-         then
-            return True;
-
-         elsif Ekind (Designator) /= E_Procedure
-           and then Is_Access_Type (Etype (Designator))
-           and then Has_Invariants (Designated_Type (Etype (Designator)))
-         then
-            return True;
-         end if;
-
-         --  Check parameters
-
-         Formal := First_Formal (Designator);
-         while Present (Formal) loop
-            if Ekind (Formal) /= E_In_Parameter
-              and then (Has_Invariants (Etype (Formal))
-                         or else Present (Predicate_Function (Etype (Formal))))
-            then
-               return True;
-
-            elsif Is_Access_Type (Etype (Formal))
-              and then Has_Invariants (Designated_Type (Etype (Formal)))
-            then
-               return True;
-            end if;
-
-            Next_Formal (Formal);
-         end loop;
-
-         return False;
-      end Invariants_Or_Predicates_Present;
-
       ------------------------------
       -- Is_Public_Subprogram_For --
       ------------------------------
@@ -11986,6 +11934,14 @@ 
          end if;
       end Is_Public_Subprogram_For;
 
+      --  Local variables
+
+      Formal     : Node_Id;
+      Formal_Typ : Entity_Id;
+      Func_Typ   : Entity_Id;
+      Post_Proc  : Entity_Id;
+      Result     : Node_Id;
+
    --  Start of processing for Process_PPCs
 
    begin
@@ -11997,10 +11953,18 @@ 
          Designator := Body_Id;
       end if;
 
+      --  Do not process a predicate function as its body will contain a
+      --  recursive call to itself and blow up the stack.
+
+      if Ekind (Designator) = E_Function
+        and then Is_Predicate_Function (Designator)
+      then
+         return;
+
       --  Internally generated subprograms, such as type-specific functions,
       --  don't get assertion checks.
 
-      if Get_TSS_Name (Designator) /= TSS_Null then
+      elsif Get_TSS_Name (Designator) /= TSS_Null then
          return;
       end if;
 
@@ -12153,10 +12117,6 @@ 
                --  Capture postcondition pragmas
 
                if Pragma_Name (Prag) = Name_Postcondition then
-                  if Plist = No_List then
-                     Plist := Empty_List;
-                  end if;
-
                   Analyze (Prag);
 
                   --  If expansion is disabled, as in a generic unit, save
@@ -12165,7 +12125,7 @@ 
                   if not Expander_Active then
                      Prepend (Grab_PPC, Declarations (N));
                   else
-                     Append (Grab_PPC, Plist);
+                     Append_Enabled_Item (Grab_PPC, Plist);
                   end if;
                end if;
 
@@ -12244,14 +12204,10 @@ 
                   if Pragma_Name (Prag) = Name_Postcondition
                     and then (not Class or else Class_Present (Prag))
                   then
-                     if Plist = No_List then
-                        Plist := Empty_List;
-                     end if;
-
                      if not Expander_Active then
                         Prepend (Grab_PPC (Pspec), Declarations (N));
                      else
-                        Append (Grab_PPC (Pspec), Plist);
+                        Append_Enabled_Item (Grab_PPC (Pspec), Plist);
                      end if;
                   end if;
 
@@ -12285,147 +12241,126 @@ 
          end Spec_Postconditions;
       end if;
 
-      --  If we had any postconditions and expansion is enabled, or if the
-      --  subprogram has invariants, then build the _Postconditions procedure.
+      --  Add an invariant call to check the result of a function
 
-      if Expander_Active
-        and then (Invariants_Or_Predicates_Present
-                   or else (Present (Plist)
-                             and then Contains_Enabled_Pragmas (Plist)))
+      if Ekind (Designator) /= E_Procedure
+        and then Expander_Active
+        and then Assertions_Enabled
       then
-         if No (Plist) then
-            Plist := Empty_List;
-         end if;
+         Func_Typ := Etype (Designator);
+         Result   := Make_Defining_Identifier (Loc, Name_uResult);
 
-         --  Special processing for function return
+         Set_Etype (Result, Func_Typ);
 
-         if Ekind (Designator) /= E_Procedure then
-            declare
-               Rent : constant Entity_Id :=
-                        Make_Defining_Identifier (Loc, Name_uResult);
-               Ftyp : constant Entity_Id := Etype (Designator);
+         --  Add argument for return
 
-            begin
-               Set_Etype (Rent, Ftyp);
+         Parms := New_List (
+           Make_Parameter_Specification (Loc,
+             Defining_Identifier => Result,
+             Parameter_Type      => New_Occurrence_Of (Func_Typ, Loc)));
 
-               --  Add argument for return
+         --  Add invariant call if returning type with invariants and this is a
+         --  public function, i.e. a function declared in the visible part of
+         --  the package defining the private type.
 
-               Parms :=
-                 New_List (
-                   Make_Parameter_Specification (Loc,
-                     Parameter_Type      => New_Occurrence_Of (Ftyp, Loc),
-                     Defining_Identifier => Rent));
+         if Has_Invariants (Func_Typ)
+           and then Present (Invariant_Procedure (Func_Typ))
+           and then Is_Public_Subprogram_For (Func_Typ)
+         then
+            Append_Enabled_Item
+              (Make_Invariant_Call (New_Occurrence_Of (Result, Loc)), Plist);
+         end if;
 
-               --  Add invariant call if returning type with invariants and
-               --  this is a public function, i.e. a function declared in the
-               --  visible part of the package defining the private type.
+         --  Same if return value is an access to type with invariants
 
-               if Has_Invariants (Etype (Rent))
-                 and then Present (Invariant_Procedure (Etype (Rent)))
-                 and then Is_Public_Subprogram_For (Etype (Rent))
-               then
-                  Append_To (Plist,
-                    Make_Invariant_Call (New_Occurrence_Of (Rent, Loc)));
-               end if;
+         Check_Access_Invariants (Result);
 
-               --  Same if return value is an access to type with invariants
+      --  Procedure case
 
-               Check_Access_Invariants (Rent);
-            end;
+      else
+         Parms := No_List;
+      end if;
 
-         --  Procedure rather than a function
+      --  Add invariant calls and predicate calls for parameters. Note that
+      --  this is done for functions as well, since in Ada 2012 they can have
+      --  IN OUT args.
 
-         else
-            Parms := No_List;
-         end if;
+      if Expander_Active and then Assertions_Enabled then
+         Formal := First_Formal (Designator);
+         while Present (Formal) loop
+            if Ekind (Formal) /= E_In_Parameter
+              or else Is_Access_Type (Etype (Formal))
+            then
+               Formal_Typ := Etype (Formal);
 
-         --  Add invariant calls and predicate calls for parameters. Note that
-         --  this is done for functions as well, since in Ada 2012 they can
-         --  have IN OUT args.
-
-         declare
-            Formal : Entity_Id;
-            Ftype  : Entity_Id;
-
-         begin
-            Formal := First_Formal (Designator);
-            while Present (Formal) loop
-               if Ekind (Formal) /= E_In_Parameter
-                 or else Is_Access_Type (Etype (Formal))
+               if Has_Invariants (Formal_Typ)
+                 and then Present (Invariant_Procedure (Formal_Typ))
+                 and then Is_Public_Subprogram_For (Formal_Typ)
                then
-                  Ftype := Etype (Formal);
+                  Append_Enabled_Item
+                    (Make_Invariant_Call (New_Occurrence_Of (Formal, Loc)),
+                     Plist);
+               end if;
 
-                  if Has_Invariants (Ftype)
-                    and then Present (Invariant_Procedure (Ftype))
-                    and then Is_Public_Subprogram_For (Ftype)
-                  then
-                     Append_To (Plist,
-                       Make_Invariant_Call
-                         (New_Occurrence_Of (Formal, Loc)));
-                  end if;
+               Check_Access_Invariants (Formal);
 
-                  Check_Access_Invariants (Formal);
-
-                  if Present (Predicate_Function (Ftype)) then
-                     Append_To (Plist,
-                       Make_Predicate_Check
-                         (Ftype, New_Occurrence_Of (Formal, Loc)));
-                  end if;
+               if Present (Predicate_Function (Formal_Typ)) then
+                  Append_Enabled_Item
+                    (Make_Predicate_Check
+                      (Formal_Typ, New_Occurrence_Of (Formal, Loc)),
+                     Plist);
                end if;
+            end if;
 
-               Next_Formal (Formal);
-            end loop;
-         end;
+            Next_Formal (Formal);
+         end loop;
+      end if;
 
-         --  Build and insert postcondition procedure
+      --  Build and insert postcondition procedure
 
-         declare
-            Post_Proc : constant Entity_Id :=
-              Make_Defining_Identifier (Loc, Chars => Name_uPostconditions);
-            --  The entity for the _Postconditions procedure
+      if Expander_Active and then Present (Plist) then
+         Post_Proc :=
+           Make_Defining_Identifier (Loc, Chars => Name_uPostconditions);
 
-         begin
-            --  Insert the corresponding body of a post condition pragma after
-            --  the last declaration of the context. This ensures that the body
-            --  will not cause any premature freezing as it may mention types:
+         --  Insert the corresponding body of a post condition pragma after the
+         --  last declaration of the context. This ensures that the body will
+         --  not cause any premature freezing as it may mention types:
 
-            --    procedure Proc (Obj : Array_Typ) is
-            --       procedure _postconditions is
-            --       begin
-            --          ... Obj ...
-            --       end _postconditions;
+         --    procedure Proc (Obj : Array_Typ) is
+         --       procedure _postconditions is
+         --       begin
+         --          ... Obj ...
+         --       end _postconditions;
 
-            --       subtype T is Array_Typ (Obj'First (1) .. Obj'Last (1));
-            --    begin
+         --       subtype T is Array_Typ (Obj'First (1) .. Obj'Last (1));
+         --    begin
 
-            --  In the example above, Obj is of type T but the incorrect
-            --  placement of _postconditions will cause a crash in gigi due to
-            --  an out of order reference. The body of _postconditions must be
-            --  placed after the declaration of Temp to preserve correct
-            --  visibility.
+         --  In the example above, Obj is of type T but the incorrect placement
+         --  of _postconditions will cause a crash in gigi due to an out of
+         --  order reference. The body of _postconditions must be placed after
+         --  the declaration of Temp to preserve correct visibility.
 
-            Insert_After_Last_Declaration (
-              Make_Subprogram_Body (Loc,
-                Specification =>
-                  Make_Procedure_Specification (Loc,
-                    Defining_Unit_Name => Post_Proc,
-                    Parameter_Specifications => Parms),
+         Insert_After_Last_Declaration (
+           Make_Subprogram_Body (Loc,
+             Specification              =>
+               Make_Procedure_Specification (Loc,
+                 Defining_Unit_Name       => Post_Proc,
+                 Parameter_Specifications => Parms),
 
-                Declarations => Empty_List,
+             Declarations               => Empty_List,
 
-                Handled_Statement_Sequence =>
-                  Make_Handled_Sequence_Of_Statements (Loc,
-                    Statements => Plist)));
+             Handled_Statement_Sequence =>
+               Make_Handled_Sequence_Of_Statements (Loc,
+                 Statements => Plist)));
 
-            Set_Ekind (Post_Proc, E_Procedure);
+         Set_Ekind (Post_Proc, E_Procedure);
 
-            --  If this is a procedure, set the Postcondition_Proc attribute on
-            --  the proper defining entity for the subprogram.
+         --  If this is a procedure, set the Postcondition_Proc attribute on
+         --  the proper defining entity for the subprogram.
 
-            if Ekind (Designator) = E_Procedure then
-               Set_Postcondition_Proc (Designator, Post_Proc);
-            end if;
-         end;
+         if Ekind (Designator) = E_Procedure then
+            Set_Postcondition_Proc (Designator, Post_Proc);
+         end if;
 
          Set_Has_Postconditions (Designator);
       end if;