ada: Missing precondition runtime check in inherited primitive

When a derived tagged type implements interface types in addition
to deriving from its parent type, and a primitive inherited from
its parent type corresponds to an inherited primitive that has
class-wide preconditions, then the generated code fails to check
the class-wide preconditions inherited from the interface primitive.

gcc/ada/ChangeLog:

	* einfo.ads (Is_Dispatch_Table_Wrapper): Complete documentation.
	* exp_ch6.adb (Install_Class_Preconditions_Check): Dispatch table
	wrappers do not require installing the check since it is performed
	by the caller.
	(Class_Preconditions_Subprogram): Use new predicate Is_LSP_Wrapper.
	* freeze.adb (Check_Inherited_Conditions): Rename Postcond_Wrappers to
	Condition_Wrappers to handle implicitly inherited subprograms that
	implement pre-/postconditions inherited from interface primitives.
	Use new predicate Is_LSP_Wrapper.
	* sem_disp.adb (Check_Dispatching_Operation): Complete assertion to
	handle functions returning class-wide types.
	* exp_util.ads (Is_LSP_Wrapper): New subprogram.
	* exp_util.adb (Is_LSP_Wrapper): New subprogram.
	* contracts.adb (Process_Spec_Postconditions): Use Is_LSP_Wrapper.
	(Process_Inherited_Conditions): Use Is_LSP_Wrapper.
	* sem_ch6.adb (New_Overloaded_Entity): Use Is_LSP_Wrapper.
	* sem_util.adb (Nearest_Class_Condition_Subprogram): Use Is_LSP_Wrapper.

9 files changed, 115 insertions, 56 deletions

diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb
index a93bf62..7e66a54 100644
--- a/gcc/ada/contracts.adb
+++ b/gcc/ada/contracts.adb
@@ -2934,9 +2934,7 @@ package body Contracts is
                --  Wrappers of class-wide pre/postconditions reference the
                --  parent primitive that has the inherited contract.
 
-               if Is_Wrapper (Subp_Id)
-                 and then Present (LSP_Subprogram (Subp_Id))
-               then
+               if Is_LSP_Wrapper (Subp_Id) then
                   Subp_Id := LSP_Subprogram (Subp_Id);
                end if;
 
@@ -4602,9 +4600,7 @@ package body Contracts is
                --  parent primitive that has the inherited contract and help
                --  us to climb fast.
 
-               if Is_Wrapper (Subp_Id)
-                 and then Present (LSP_Subprogram (Subp_Id))
-               then
+               if Is_LSP_Wrapper (Subp_Id) then
                   Subp_Id := LSP_Subprogram (Subp_Id);
                end if;
 
diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads
index 2fb4570..2aae60a 100644
--- a/gcc/ada/einfo.ads
+++ b/gcc/ada/einfo.ads
@@ -2576,9 +2576,12 @@ package Einfo is
 --       entity is associated with a dispatch table.
 
 --    Is_Dispatch_Table_Wrapper
---       Applies to all entities. Set on wrappers built when the subprogram has
---       class-wide preconditions or class-wide postconditions affected by
---       overriding (AI12-0195).
+--       Applies to all entities. Set on wrappers built when a subprogram has
+--       class-wide preconditions or postconditions affected by overriding
+--       (AI12-0195). Also set on wrappers built when an inherited subprogram
+--       implements an interface primitive that has class-wide preconditions
+--       or postconditions. In the former case, the entity also has its
+--       LSP_Subprogram attribute set.
 
 --    Is_Dispatching_Operation
 --       Defined in all entities. Set for procedures, functions, generic
diff --git a/gcc/ada/exp_ch6.adb b/gcc/ada/exp_ch6.adb
index c550b1c..3843244 100644
--- a/gcc/ada/exp_ch6.adb
+++ b/gcc/ada/exp_ch6.adb
@@ -7748,9 +7748,7 @@ package body Exp_Ch6 is
                --  Wrappers of class-wide pre/postconditions reference the
                --  parent primitive that has the inherited contract.
 
-               if Is_Wrapper (Subp_Id)
-                 and then Present (LSP_Subprogram (Subp_Id))
-               then
+               if Is_LSP_Wrapper (Subp_Id) then
                   Subp_Id := LSP_Subprogram (Subp_Id);
                end if;
 
@@ -7796,6 +7794,35 @@ package body Exp_Ch6 is
 
       elsif Is_Thunk (Current_Scope) then
          return;
+
+      --  The call to the inherited primitive in a dispatch table wrapper must
+      --  not have the class-wide precondition check since it is installed in
+      --  the caller of the wrapper. This is also required to avoid the wrong
+      --  evaluation of class-wide preconditions in Condition_Wrappers (ie.
+      --  wrappers of inherited primitives that implement additional interface
+      --  primitives that have preconditions).
+
+      --  For example:
+      --    type Typ is tagged null record;
+      --    procedure Prim (X : T) with Pre'Class => False;
+
+      --    type Iface is interface;
+      --    procedure Prim (X : Iface) is abstract with Pre'Class => True;
+
+      --    type DT is new Typ and Iface with null record;
+      --    <internally built dispatch table wrapper of inherited Prim>
+
+      --  The class-wide preconditions of the wrapper must not fail due to the
+      --  disjunction of the class-wide preconditions of subprograms Typ.Prim
+      --  and Iface.Prim. If the precondition check were placed in the
+      --  wrapper's call to the inherited parent primitive, its class-wide
+      --  condition would incorrectly be reported as failed at runtime.
+
+      elsif Is_Dispatch_Table_Wrapper (Current_Scope)
+        or else (Chars (Current_Scope) = Name_uWrapped_Statements
+                   and then Is_Dispatch_Table_Wrapper (Scope (Current_Scope)))
+      then
+         return;
       end if;
 
       Subp := Entity (Name (Call_Node));
diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb
index 400d5d8..4029ea6 100644
--- a/gcc/ada/exp_util.adb
+++ b/gcc/ada/exp_util.adb
@@ -9193,6 +9193,16 @@ package body Exp_Util is
       return Is_Tagged_Type (Typ) and then Is_Library_Level_Entity (Typ);
    end Is_Library_Level_Tagged_Type;
 
+   --------------------
+   -- Is_LSP_Wrapper --
+   --------------------
+
+   function Is_LSP_Wrapper (E : Entity_Id) return Boolean is
+   begin
+      return Is_Dispatch_Table_Wrapper (E)
+        and then Present (LSP_Subprogram (E));
+   end Is_LSP_Wrapper;
+
    --------------------------
    -- Is_Non_BIP_Func_Call --
    --------------------------
diff --git a/gcc/ada/exp_util.ads b/gcc/ada/exp_util.ads
index 49e75c7..898d712 100644
--- a/gcc/ada/exp_util.ads
+++ b/gcc/ada/exp_util.ads
@@ -789,6 +789,11 @@ package Exp_Util is
    --  Return True if Typ is a library level tagged type. Currently we use
    --  this information to build statically allocated dispatch tables.
 
+   function Is_LSP_Wrapper (E : Entity_Id) return Boolean;
+   --  Return True if E is a wrapper built when a subprogram has class-wide
+   --  preconditions or postconditions affected by overriding (AI12-0195).
+   --  LSP stands for Liskov Substitution Principle.
+
    function Is_Non_BIP_Func_Call (Expr : Node_Id) return Boolean;
    --  Determine whether node Expr denotes a non build-in-place function call
 
diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb
index 9c14e1f1..c7e3be0 100644
--- a/gcc/ada/freeze.adb
+++ b/gcc/ada/freeze.adb
@@ -1463,7 +1463,7 @@ package body Freeze is
       Par_Prim       : Entity_Id;
       Prim           : Entity_Id;
 
-      type Wrapper_Kind is (No_Wrapper, LSP_Wrapper, Postcond_Wrapper);
+      type Wrapper_Kind is (No_Wrapper, LSP_Wrapper, Condition_Wrapper);
 
       Wrapper_Needed : Wrapper_Kind;
       --  Kind of wrapper needed by a given inherited primitive of tagged
@@ -1471,8 +1471,9 @@ package body Freeze is
       --  * No_Wrapper: No wrapper is needed.
       --  * LSP_Wrapper: Wrapper that handles inherited class-wide pre/post
       --    conditions that call overridden primitives.
-      --  * Postcond_Wrapper: Wrapper that handles postconditions of interface
-      --    primitives.
+      --  * Condition_Wrapper: Wrapper of inherited subprogram that implements
+      --    additional interface primitives of the derived type that have
+      --    class-wide pre-/postconditions.
 
       function Build_DTW_Body
         (Loc          : Source_Ptr;
@@ -1855,9 +1856,9 @@ package body Freeze is
       --  List containing identifiers of built wrappers. Used to defer building
       --  and analyzing their class-wide precondition subprograms.
 
-      Postcond_Candidates_List : Elist_Id := No_Elist;
+      Condition_Candidates_List : Elist_Id := No_Elist;
       --  List containing inherited primitives of tagged type R that implement
-      --  interface primitives that have postconditions.
+      --  interface primitives that have pre-/postconditions.
 
    --  Start of processing for Check_Inherited_Conditions
 
@@ -1907,9 +1908,7 @@ package body Freeze is
             --  When the primitive is an LSP wrapper we climb to the parent
             --  primitive that has the inherited contract.
 
-            if Is_Wrapper (Par_Prim)
-              and then Present (LSP_Subprogram (Par_Prim))
-            then
+            if Is_LSP_Wrapper (Par_Prim) then
                Par_Prim := LSP_Subprogram (Par_Prim);
             end if;
 
@@ -1943,7 +1942,7 @@ package body Freeze is
       end loop;
 
       --  Collect inherited primitives that may need a wrapper to handle
-      --  postconditions of interface primitives; done to improve the
+      --  pre-/postconditions of interface primitives; done to improve the
       --  performance when checking if postcondition wrappers are needed.
 
       Op_Node := First_Elmt (Prim_Ops);
@@ -1952,13 +1951,16 @@ package body Freeze is
 
          if Present (Interface_Alias (Prim))
            and then not Comes_From_Source (Alias (Prim))
-           and then Present (Class_Postconditions (Interface_Alias (Prim)))
+           and then
+             (Present (Class_Preconditions (Interface_Alias (Prim)))
+                or else
+              Present (Class_Postconditions (Interface_Alias (Prim))))
          then
-            if No (Postcond_Candidates_List) then
-               Postcond_Candidates_List := New_Elmt_List;
+            if No (Condition_Candidates_List) then
+               Condition_Candidates_List := New_Elmt_List;
             end if;
 
-            Append_Unique_Elmt (Alias (Prim), Postcond_Candidates_List);
+            Append_Unique_Elmt (Alias (Prim), Condition_Candidates_List);
          end if;
 
          Next_Elmt (Op_Node);
@@ -1986,9 +1988,7 @@ package body Freeze is
             --  When the primitive is an LSP wrapper we climb to the parent
             --  primitive that has the inherited contract.
 
-            if Is_Wrapper (Par_Prim)
-              and then Present (LSP_Subprogram (Par_Prim))
-            then
+            if Is_LSP_Wrapper (Par_Prim) then
                Par_Prim := LSP_Subprogram (Par_Prim);
             end if;
 
@@ -2014,12 +2014,12 @@ package body Freeze is
             --  implements additional interface types, and this inherited
             --  primitive covers an interface primitive of these additional
             --  interface types that has class-wide postconditions, then it
-            --  requires a postconditions wrapper.
+            --  requires a pre-/postconditions wrapper.
 
             if Wrapper_Needed = No_Wrapper
               and then Present (Interfaces (R))
-              and then Present (Postcond_Candidates_List)
-              and then Contains (Postcond_Candidates_List, Prim)
+              and then Present (Condition_Candidates_List)
+              and then Contains (Condition_Candidates_List, Prim)
             then
                declare
                   Elmt       : Elmt_Id;
@@ -2029,7 +2029,8 @@ package body Freeze is
 
                begin
                   Elmt := First_Elmt (Prim_Ops);
-                  while Present (Elmt) loop
+
+                  Search : while Present (Elmt) loop
                      Ent := Node (Elmt);
 
                      --  Perform the search relying on the internal entities
@@ -2039,7 +2040,9 @@ package body Freeze is
                      if Present (Interface_Alias (Ent))
                        and then (Alias (Ent)) = Prim
                        and then
-                         Present (Class_Postconditions (Interface_Alias (Ent)))
+                         (Present (Class_Preconditions (Interface_Alias (Ent)))
+                            or else Present (Class_Postconditions
+                                               (Interface_Alias (Ent))))
                      then
                         Iface := Find_Dispatching_Type (Interface_Alias (Ent));
 
@@ -2052,8 +2055,8 @@ package body Freeze is
                         Iface_Elmt := First_Elmt (Interfaces (R));
                         while Present (Iface_Elmt) loop
                            if Node (Iface_Elmt) = Iface then
-                              Wrapper_Needed := Postcond_Wrapper;
-                              exit;
+                              Wrapper_Needed := Condition_Wrapper;
+                              exit Search;
                            end if;
 
                            Next_Elmt (Iface_Elmt);
@@ -2061,7 +2064,7 @@ package body Freeze is
                      end if;
 
                      Next_Elmt (Elmt);
-                  end loop;
+                  end loop Search;
                end;
             end if;
          end if;
@@ -2108,7 +2111,8 @@ package body Freeze is
 
                --  LSP wrappers reference the parent primitive that has the
                --  the class-wide pre/post condition that calls overridden
-               --  primitives.
+               --  primitives. Condition wrappers do not have this attribute
+               --  (see predicate Is_LSP_Wrapper).
 
                if Wrapper_Needed = LSP_Wrapper then
                   Set_LSP_Subprogram (DTW_Id, Par_Prim);
@@ -2124,11 +2128,12 @@ package body Freeze is
 
                Set_Sloc (DTW_Id, Sloc (Prim));
 
-               --  For inherited class-wide preconditions the DTW wrapper
-               --  reuses the ICW of the parent (which checks the parent
-               --  interpretation of the class-wide preconditions); the
-               --  interpretation of the class-wide preconditions for the
-               --  inherited subprogram is checked at the caller side.
+               --  For LSP_Wrappers of subprograms that inherit class-wide
+               --  preconditions the DTW wrapper reuses the ICW of the parent
+               --  (which checks the parent interpretation of the class-wide
+               --  preconditions); the interpretation of the class-wide
+               --  preconditions for the inherited subprogram is checked
+               --  at the caller side.
 
                --  When the subprogram inherits class-wide postconditions
                --  the DTW also checks the interpretation of the class-wide
@@ -2137,12 +2142,14 @@ package body Freeze is
                --  the class-wide postconditions.
 
                --      procedure Prim (F1 : T1; ...) is
-               --         [ pragma Check (Postcondition, Expr); ]
+               --         [ pragma Postcondition (check => Expr); ]
                --      begin
                --         Par_Prim_ICW (Par_Type (F1), ...);
                --      end;
 
-               if Present (Indirect_Call_Wrapper (Par_Prim)) then
+               if Wrapper_Needed = LSP_Wrapper
+                 and then Present (Indirect_Call_Wrapper (Par_Prim))
+               then
                   DTW_Body :=
                     Build_DTW_Body (Loc,
                       DTW_Spec     => DTW_Spec,
@@ -2150,19 +2157,27 @@ package body Freeze is
                       Par_Prim     => Par_Prim,
                       Wrapped_Subp => Indirect_Call_Wrapper (Par_Prim));
 
-               --  For subprograms that only inherit class-wide postconditions
-               --  the DTW wrapper calls the parent primitive (which on its
-               --  body checks the interpretation of the class-wide post-
-               --  conditions for the parent subprogram), and the DTW checks
-               --  the interpretation of the class-wide postconditions for the
+               --  For LSP_Wrappers of subprograms that only inherit class-wide
+               --  postconditions, and also for Condition_Wrappers (wrappers of
+               --  inherited subprograms that implement additional interface
+               --  primitives that have class-wide pre-/postconditions), the
+               --  DTW wrapper calls the parent primitive (which on its body
+               --  checks the interpretation of the class-wide post-conditions
+               --  for the parent subprogram), and the DTW checks the
+               --  interpretation of the class-wide postconditions for the
                --  inherited subprogram.
 
                --      procedure Prim (F1 : T1; ...) is
-               --         pragma Check (Postcondition, Expr);
+               --         pragma Postcondition (check => Expr);
                --      begin
                --         Par_Prim (Par_Type (F1), ...);
                --      end;
 
+               --  No class-wide preconditions runtime check is generated for
+               --  this wrapper call to the parent primitive, since the check
+               --  is performed by the caller of the DTW wrapper (see routine
+               --  Install_Class_Preconditions_Check).
+
                else
                   DTW_Body :=
                     Build_DTW_Body (Loc,
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index 8cf191d..944f5ca 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -12651,9 +12651,7 @@ package body Sem_Ch6 is
                   --  chain of ancestor primitives (see Map_Primitives). They
                   --  don't inherit contracts.
 
-                  if Is_Wrapper (S)
-                    and then Present (LSP_Subprogram (S))
-                  then
+                  if Is_LSP_Wrapper (S) then
                      Set_Overridden_Operation (S, Ultimate_Alias (E));
 
                   --  For entities generated by Derive_Subprograms the
diff --git a/gcc/ada/sem_disp.adb b/gcc/ada/sem_disp.adb
index 203e914..971192c 100644
--- a/gcc/ada/sem_disp.adb
+++ b/gcc/ada/sem_disp.adb
@@ -1458,9 +1458,16 @@ package body Sem_Disp is
             pragma Assert
               ((Ekind (Subp) = E_Function
                  and then Is_Dispatching_Operation (Old_Subp)
+                 and then not Is_Class_Wide_Type (Etype (Subp))
                  and then Is_Null_Extension (Base_Type (Etype (Subp))))
 
               or else
+               (Ekind (Subp) = E_Function
+                 and then Is_Dispatching_Operation (Old_Subp)
+                 and then Is_Class_Wide_Type (Etype (Subp))
+                 and then Is_Null_Extension (Root_Type (Etype (Subp))))
+
+              or else
                (Ekind (Subp) = E_Procedure
                  and then Is_Dispatching_Operation (Old_Subp)
                  and then Present (Alias (Old_Subp))
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index 5c32b0b..5d3a4e6 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -22246,9 +22246,7 @@ package body Sem_Util is
             --  Wrappers of class-wide pre/postconditions reference the
             --  parent primitive that has the inherited contract.
 
-            if Is_Wrapper (Subp_Id)
-              and then Present (LSP_Subprogram (Subp_Id))
-            then
+            if Is_LSP_Wrapper (Subp_Id) then
                Subp_Id := LSP_Subprogram (Subp_Id);
             end if;