Patchwork [Ada] Implementation of pre/postconditions for entries

login
register
mail settings
Submitter Arnaud Charlet
Date Oct. 18, 2010, 10:11 a.m.
Message ID <20101018101103.GA12178@adacore.com>
Download mbox | patch
Permalink /patch/68162/
State New
Headers show

Comments

Arnaud Charlet - Oct. 18, 2010, 10:11 a.m.
This patch completes the implementation of Ada2012 AI-145. Pre/postconditions
that are aspects of task and protected entries are evaluated in a wrapper
procedure that incorporates the original entry call.

Executing the program below with:

   gnatmake -gnat12 -gnata prepostentry
   prepostentry

must yield:

proper protected call
 46
protected entry call violates precondition
10: failed precondition from prepostentry.adb:27
protected entry call violates postcondition
10: failed postcondition from prepostentry.adb:28
 46
task entry  call violates precondition
10: failed precondition from prepostentry.adb:10
task entry  call violates postcondition
10: failed postcondition from prepostentry.adb:11
------

pragma Ada_2012;

with Ada.Assertions; use Ada.Assertions;
with Ada.Exceptions; use Ada.Exceptions;
with Ada.Text_IO;    use Ada.Text_IO;

procedure PrePostEntry is
   task type TT (Disc : Integer) is
      entry MyEntry (A : in out Integer) with
        Pre  => A > Disc,
        Post => A = A'Old + 1;
   end TT;

   task body TT is
   begin
      for J in 1 .. 2 loop
      accept MyEntry (A : in out Integer) do
         if A /= 17 then
            A := A + 1;
         end if;
      end;
      end loop;
   end TT;

   protected type PP is
      entry MyEntry (A : in out Integer) with
        Pre  => A > 10,
        Post => A = A'Old + 1;
   end PP;

   protected body PP is
      entry MyEntry (A : in out Integer) when True is
      begin
         if A /= 17 then
            A := A + 1;
         end if;
      end Myentry;
   end;

   MyTask : TT (10);
   Hval   : Integer;

   MyProt : PP;

begin
   Put_Line ("proper protected call");
   Hval := 45;
   MyProt.MyEntry (Hval);
   Put_Line (Integer'Image (Hval));

   begin
      Put_Line ("protected entry call violates precondition");
      Hval := 10;
      MyProt.MyEntry (Hval);
   exception
      when E : Assertion_Error =>
         Put_Line ("10: " & Exception_Message (E));
   end;

   begin
      Put_Line ("protected entry call violates postcondition");
      Hval := 17;
      MyProt.MyEntry (Hval);
   exception
      when E : Assertion_Error =>
         Put_Line ("10: " & Exception_Message (E));
   end;

   Hval := 45;
   MyTask.MyEntry (Hval);
   Put_Line (Integer'Image (Hval));

   begin
      Put_Line ("task entry  call violates precondition");
      Hval := 10;
      MyTask.MyEntry (Hval);
   exception
      when E : Assertion_Error =>
         Put_Line ("10: " & Exception_Message (E));
   end;

   begin
      Put_Line ("task entry  call violates postcondition");
      Hval := 17;
      MyTask.MyEntry (Hval);
   exception
      when E : Assertion_Error =>
         Put_Line ("10: " & Exception_Message (E));
   end;

end PrePostEntry;

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

2010-10-18  Ed Schonberg  <schonberg@adacore.com>

	* einfo.ads, einfo.adb: New attribute PPC_Wrapper for entries and entry
	families. Denotes a procedure that performs pre/postcondition checks
	and then performs the entry call.
	* sem_res.adb (Resolve_Entry_Call): If the entry has
	pre/postconditions, replace call with a call to the PPC_Wrapper of the
	entry.
	* exp_ch9.adb (Build_PPC_Wrapper): new procedure.
	(Expand_N_Entry_Declaration, Expand_N_Protected_Type_Declaration): call
	Build_PPC_Wrapper for all entries in task and protected definitions.

Patch

Index: exp_ch9.adb
===================================================================
--- exp_ch9.adb	(revision 165610)
+++ exp_ch9.adb	(working copy)
@@ -162,6 +162,14 @@  package body Exp_Ch9 is
    --       <formalN> : AnnN;
    --    end record;
 
+   procedure Build_PPC_Wrapper (E : Entity_Id; Decl : Node_Id);
+   --  Build body of wrapper procedure for an entry or entry family that has
+   --  pre/postconditions. The body gathers the PPC's and expands them in the
+   --  usual way, and performs the entry call itself. This way preconditions
+   --  are evaluated before the call is queued. E is the entry in question,
+   --  and Decl is the enclosing synchronized type declaration at whose
+   --  freeze point the generated body is analyzed.
+
    procedure Build_Wrapper_Bodies
      (Loc : Source_Ptr;
       Typ : Entity_Id;
@@ -1568,6 +1576,147 @@  package body Exp_Ch9 is
       return Rec_Nam;
    end Build_Parameter_Block;
 
+   -----------------------
+   -- Build_PPC_Wrapper --
+   -----------------------
+
+   procedure Build_PPC_Wrapper (E : Entity_Id; Decl : Node_Id) is
+      Loc        : constant Source_Ptr := Sloc (E);
+      Synch_Type : constant Entity_Id := Scope (E);
+
+      Wrapper_Id : constant Entity_Id :=
+                     Make_Defining_Identifier (Loc,
+                       Chars => New_External_Name (Chars (E), 'E'));
+      --  the wrapper procedure name
+
+      Wrapper_Body : Node_Id;
+
+      Synch_Id : constant Entity_Id :=
+                   Make_Defining_Identifier (Loc,
+                     Chars => New_External_Name (Chars (Scope (E)), 'A'));
+      --  The parameter that designates the synchronized object in the call
+
+      Actuals : constant List_Id := New_List;
+      --  the actuals in the entry call.
+
+      Entry_Call : constant Node_Id :=
+                     Make_Procedure_Call_Statement (Loc,
+                       Name =>
+                         Make_Selected_Component (Loc,
+                           Prefix        => New_Occurrence_Of (Synch_Id, Loc),
+                           Selector_Name => New_Occurrence_Of (E, Loc)),
+                       Parameter_Associations => Actuals);
+
+      Decls      : constant List_Id := New_List;
+
+      Specs : List_Id;
+      --  The specification of the wrapper procedure
+
+   begin
+
+      --  Only build the wrapper if entry has pre/postconditions.
+      --  Should this be done unconditionally instead ???
+
+      declare
+         P : Node_Id;
+
+      begin
+         P := Spec_PPC_List (E);
+         if No (P) then
+            return;
+         end if;
+
+         --  Transfer ppc pragmas to the declarations of the wrapper
+
+         while Present (P) loop
+            if Pragma_Name (P) = Name_Precondition
+              or else Pragma_Name (P) = Name_Postcondition
+            then
+               Append (Relocate_Node (P), Decls);
+               Set_Analyzed (Last (Decls), False);
+            end if;
+
+            P := Next_Pragma (P);
+         end loop;
+      end;
+
+      --  First formal is synchronized object
+
+      Specs := New_List (
+        Make_Parameter_Specification (Loc,
+          Defining_Identifier => Synch_Id,
+          Out_Present         =>  True,
+          In_Present          =>  True,
+          Parameter_Type      => New_Occurrence_Of (Scope (E), Loc)));
+
+      --  Now add formals that match those of the entry, and build actuals
+      --  for the nested entry call.
+
+      declare
+         Form      : Entity_Id;
+         New_Form  : Entity_Id;
+         Parm_Spec : Node_Id;
+
+      begin
+         Form := First_Formal (E);
+         while Present (Form) loop
+            New_Form := Make_Defining_Identifier (Loc, Chars (Form));
+            Parm_Spec :=
+              Make_Parameter_Specification (Loc,
+                Defining_Identifier => New_Form,
+                Out_Present         =>  Out_Present (Parent (Form)),
+                In_Present          =>  In_Present  (Parent (Form)),
+                Parameter_Type      => New_Occurrence_Of (Etype (Form), Loc));
+
+            Append (Parm_Spec, Specs);
+            Append (New_Occurrence_Of (New_Form, Loc), Actuals);
+            Next_Formal (Form);
+         end loop;
+      end;
+
+      --  Add renaming declarations for the discriminants of the enclosing
+      --  type, which may be visible in the preconditions.
+
+      if Has_Discriminants (Synch_Type) then
+         declare
+            D : Entity_Id;
+            Decl : Node_Id;
+
+         begin
+            D := First_Discriminant (Synch_Type);
+            while Present (D) loop
+               Decl :=
+                 Make_Object_Renaming_Declaration (Loc,
+                   Defining_Identifier =>
+                     Make_Defining_Identifier (Loc, Chars (D)),
+                   Subtype_Mark        => New_Reference_To (Etype (D), Loc),
+                   Name                =>
+                     Make_Selected_Component (Loc,
+                       Prefix        => New_Reference_To (Synch_Id, Loc),
+                       Selector_Name => Make_Identifier (Loc, Chars (D))));
+               Prepend (Decl, Decls);
+               Next_Discriminant (D);
+            end loop;
+         end;
+      end if;
+
+      Set_PPC_Wrapper (E, Wrapper_Id);
+      Wrapper_Body :=
+        Make_Subprogram_Body (Loc,
+          Specification =>
+            Make_Procedure_Specification (Loc,
+              Defining_Unit_Name => Wrapper_Id,
+              Parameter_Specifications => Specs),
+         Declarations => Decls,
+         Handled_Statement_Sequence =>
+           Make_Handled_Sequence_Of_Statements (Loc,
+             Statements => New_List (Entry_Call)));
+
+      --  The wrapper body is analyzed when the enclosing type is frozen.
+
+      Append_Freeze_Action (Defining_Entity (Decl), Wrapper_Body);
+   end Build_PPC_Wrapper;
+
    --------------------------
    -- Build_Wrapper_Bodies --
    --------------------------
@@ -1613,11 +1762,11 @@  package body Exp_Ch9 is
          end if;
 
          declare
-            Actuals      : List_Id := No_List;
-            Conv_Id      : Node_Id;
-            First_Form   : Node_Id;
-            Formal       : Node_Id;
-            Nam          : Node_Id;
+            Actuals    : List_Id := No_List;
+            Conv_Id    : Node_Id;
+            First_Form : Node_Id;
+            Formal     : Node_Id;
+            Nam        : Node_Id;
 
          begin
             --  Map formals to actuals. Use the list built for the wrapper
@@ -1630,7 +1779,6 @@  package body Exp_Ch9 is
 
             if Present (Formal) then
                Actuals := New_List;
-
                while Present (Formal) loop
                   Append_To (Actuals,
                     Make_Identifier (Loc, Chars =>
@@ -1653,9 +1801,9 @@  package body Exp_Ch9 is
 
                if Is_Controlling_Formal (First_Formal (Subp_Id)) then
                   Prepend_To (Actuals,
-                    Unchecked_Convert_To (
-                      Corresponding_Concurrent_Type (Obj_Typ),
-                      Make_Identifier (Loc, Name_uO)));
+                    Unchecked_Convert_To
+                      (Corresponding_Concurrent_Type (Obj_Typ),
+                       Make_Identifier (Loc, Name_uO)));
 
                else
                   Prepend_To (Actuals,
@@ -1685,11 +1833,9 @@  package body Exp_Ch9 is
                Nam :=
                  Make_Selected_Component (Loc,
                    Prefix =>
-                     Unchecked_Convert_To (
-                       Corresponding_Concurrent_Type (Obj_Typ),
-                       Conv_Id),
-                   Selector_Name =>
-                     New_Reference_To (Subp_Id, Loc));
+                     Unchecked_Convert_To
+                       (Corresponding_Concurrent_Type (Obj_Typ), Conv_Id),
+                   Selector_Name => New_Reference_To (Subp_Id, Loc));
             end if;
 
             --  Create the subprogram body. For a function, the call to the
@@ -8050,6 +8196,10 @@  package body Exp_Ch9 is
             Insert_After (Current_Node, Sub);
             Analyze (Sub);
 
+            --  build wrapper procedure for pre/postconditions.
+
+            Build_PPC_Wrapper (Comp_Id, N);
+
             Set_Protected_Body_Subprogram
               (Defining_Identifier (Comp),
                Defining_Unit_Name (Specification (Sub)));
@@ -10599,6 +10749,24 @@  package body Exp_Ch9 is
       --  any were declared.
 
       Expand_Previous_Access_Type (Tasktyp);
+
+      --  Create wrappers for entries that have pre/postconditions
+
+      declare
+         Ent : Entity_Id;
+
+      begin
+         Ent := First_Entity (Tasktyp);
+         while Present (Ent) loop
+            if Ekind_In (Ent, E_Entry, E_Entry_Family)
+              and then Present (Spec_PPC_List (Ent))
+            then
+               Build_PPC_Wrapper (Ent, N);
+            end if;
+
+            Next_Entity (Ent);
+         end loop;
+      end;
    end Expand_N_Task_Type_Declaration;
 
    -------------------------------
Index: einfo.adb
===================================================================
--- einfo.adb	(revision 165620)
+++ einfo.adb	(working copy)
@@ -214,6 +214,7 @@  package body Einfo is
    --    Interfaces                      Elist25
    --    Debug_Renaming_Link             Node25
    --    DT_Offset_To_Top_Func           Node25
+   --    PPC_Wrapper                     Node25
    --    Task_Body_Procedure             Node25
 
    --    Dispatch_Table_Wrappers         Elist26
@@ -512,7 +513,6 @@  package body Einfo is
    --    OK_To_Rename                    Flag247
 
    --    (unused)                        Flag232
-
    --    (unused)                        Flag248
    --    (unused)                        Flag249
    --    (unused)                        Flag250
@@ -2359,6 +2359,12 @@  package body Einfo is
       return Node8 (Id);
    end Postcondition_Proc;
 
+   function PPC_Wrapper (Id : E) return E is
+   begin
+      pragma Assert (Ekind_In (Id, E_Entry, E_Entry_Family));
+      return Node25 (Id);
+   end PPC_Wrapper;
+
    function Prival (Id : E) return E is
    begin
       pragma Assert (Is_Protected_Component (Id));
@@ -2582,7 +2588,7 @@  package body Einfo is
    function Spec_PPC_List (Id : E) return N is
    begin
       pragma Assert
-        (Ekind (Id) = E_Entry
+        (Ekind_In (Id,  E_Entry, E_Entry_Family)
           or else Is_Subprogram (Id)
           or else Is_Generic_Subprogram (Id));
       return Node24 (Id);
@@ -4817,6 +4823,12 @@  package body Einfo is
       Set_Node8 (Id, V);
    end Set_Postcondition_Proc;
 
+   procedure Set_PPC_Wrapper (Id : E; V : E) is
+   begin
+      pragma Assert (Ekind_In (Id, E_Entry, E_Entry_Family));
+      Set_Node25 (Id, V);
+   end Set_PPC_Wrapper;
+
    procedure Set_Direct_Primitive_Operations (Id : E; V : L) is
    begin
       pragma Assert
@@ -5057,7 +5069,7 @@  package body Einfo is
    procedure Set_Spec_PPC_List (Id : E; V : N) is
    begin
       pragma Assert
-        (Ekind_In (Id, E_Entry, E_Void)
+        (Ekind_In (Id, E_Entry, E_Entry_Family, E_Void)
           or else Is_Subprogram (Id)
           or else Is_Generic_Subprogram (Id));
       Set_Node24 (Id, V);
@@ -6575,16 +6587,6 @@  package body Einfo is
       return Ekind (Id);
    end Parameter_Mode;
 
-   ---------------------
-   -- Record_Rep_Item --
-   ---------------------
-
-   procedure Record_Rep_Item (E : Entity_Id; N : Node_Id) is
-   begin
-      Set_Next_Rep_Item (N, First_Rep_Item (E));
-      Set_First_Rep_Item (E, N);
-   end Record_Rep_Item;
-
    --------------------------
    -- Primitive_Operations --
    --------------------------
@@ -6603,6 +6605,16 @@  package body Einfo is
       end if;
    end Primitive_Operations;
 
+   ---------------------
+   -- Record_Rep_Item --
+   ---------------------
+
+   procedure Record_Rep_Item (E : Entity_Id; N : Node_Id) is
+   begin
+      Set_Next_Rep_Item (N, First_Rep_Item (E));
+      Set_First_Rep_Item (E, N);
+   end Record_Rep_Item;
+
    ---------------
    -- Root_Type --
    ---------------
@@ -8132,6 +8144,10 @@  package body Einfo is
          when E_Variable                                   =>
             Write_Str ("Debug_Renaming_Link");
 
+         when E_Entry                                      |
+              E_Entry_Family                               =>
+            Write_Str ("PPC_Wrapper");
+
          when others                                       =>
             Write_Str ("Field25??");
       end case;
Index: einfo.ads
===================================================================
--- einfo.ads	(revision 165618)
+++ einfo.ads	(working copy)
@@ -3211,6 +3211,11 @@  package Einfo is
 --       to generate the call to this procedure in case the expander inserts
 --       implicit return statements.
 
+--    PPC_Wrapper (Node25)
+--       Present in entries and entry families. Set only if pre- or post-
+--       conditions are present. The precondition_wrapper body is the original
+--       entry call, decorated with the given precondition for the entry.
+
 --    Primitive_Operations (synthesized)
 --       Present in concurrent types, tagged record types and subtypes, tagged
 --       private types and tagged incomplete types. For concurrent types that
@@ -4960,6 +4965,7 @@  package Einfo is
    --    Scope_Depth_Value                   (Uint22)
    --    Protection_Object                   (Node23)   (protected kind)
    --    Spec_PPC_List                       (Node24)   (for entry only)
+   --    PPC_Wrapper                         (Node25)
    --    Default_Expressions_Processed       (Flag108)
    --    Entry_Accepted                      (Flag152)
    --    Is_AST_Entry                        (Flag132)  (for entry only)
@@ -6079,6 +6085,7 @@  package Einfo is
    function Packed_Array_Type                   (Id : E) return E;
    function Parent_Subtype                      (Id : E) return E;
    function Postcondition_Proc                  (Id : E) return E;
+   function PPC_Wrapper                         (Id : E) return E;
    function Direct_Primitive_Operations         (Id : E) return L;
    function Prival                              (Id : E) return E;
    function Prival_Link                         (Id : E) return E;
@@ -6649,6 +6656,7 @@  package Einfo is
    procedure Set_Packed_Array_Type               (Id : E; V : E);
    procedure Set_Parent_Subtype                  (Id : E; V : E);
    procedure Set_Postcondition_Proc              (Id : E; V : E);
+   procedure Set_PPC_Wrapper                     (Id : E; V : E);
    procedure Set_Direct_Primitive_Operations     (Id : E; V : L);
    procedure Set_Prival                          (Id : E; V : E);
    procedure Set_Prival_Link                     (Id : E; V : E);
@@ -7367,6 +7375,7 @@  package Einfo is
    pragma Inline (Parameter_Mode);
    pragma Inline (Parent_Subtype);
    pragma Inline (Postcondition_Proc);
+   pragma Inline (PPC_Wrapper);
    pragma Inline (Prival);
    pragma Inline (Prival_Link);
    pragma Inline (Private_Dependents);
@@ -7757,6 +7766,7 @@  package Einfo is
    pragma Inline (Set_Packed_Array_Type);
    pragma Inline (Set_Parent_Subtype);
    pragma Inline (Set_Postcondition_Proc);
+   pragma Inline (Set_PPC_Wrapper);
    pragma Inline (Set_Prival);
    pragma Inline (Set_Prival_Link);
    pragma Inline (Set_Private_Dependents);
Index: sem_res.adb
===================================================================
--- sem_res.adb	(revision 165610)
+++ sem_res.adb	(working copy)
@@ -6327,6 +6327,29 @@  package body Sem_Res is
          end;
       end if;
 
+      if Ekind_In (Nam, E_Entry, E_Entry_Family)
+        and then Present (PPC_Wrapper (Nam))
+        and then Current_Scope /= PPC_Wrapper (Nam)
+      then
+
+         --  Rewrite as call to the precondition wrapper, adding the
+         --  task object to the list of actuals.
+
+         declare
+            New_Call : Node_Id;
+            New_Actuals : List_Id;
+         begin
+            New_Actuals := New_List (Obj);
+            Append_List (Parameter_Associations (N), New_Actuals);
+            New_Call := Make_Procedure_Call_Statement (Loc,
+              Name => New_Occurrence_Of (PPC_Wrapper (Nam), Loc),
+              Parameter_Associations => New_Actuals);
+            Rewrite (N, New_Call);
+            Analyze_And_Resolve (N);
+            return;
+         end;
+      end if;
+
       --  The operation name may have been overloaded. Order the actuals
       --  according to the formals of the resolved entity, and set the
       --  return type to that of the operation.