Patchwork [Ada] Quantified expressions in pre/postconditions and other contexts

login
register
mail settings
Submitter Arnaud Charlet
Date Oct. 26, 2010, 1:05 p.m.
Message ID <20101026130545.GA5227@adacore.com>
Download mbox | patch
Permalink /patch/69247/
State New
Headers show

Comments

Arnaud Charlet - Oct. 26, 2010, 1:05 p.m.
Quantified expressions over arrays typically include indexed expressions over
implicit or explicit ranges. The range checks and other code resulting from
expansion of the condition in a quantified expression must be inserted at the
proper places in the tree. This patch generalizes the mechanism that handles
discrete ranges, which previously only appeared in loops and type declarations.
With this patch quantified expressions are handled properly when they appear
within preconditions and Assert statements.
The following must compile quietly;

      gcc -c -gnat12 -gnata ex1.adb
---
package Ex1 is
   type Extended_Index is range 0 .. 10_000;
   subtype Index is Extended_Index range 1 .. Extended_Index'Last;
   type Arr is array (Index range <>) of Natural;

   function Find_Array (A : Arr; Query : Natural) return Extended_Index with
     Pre  => (for some J in A'Range => (A (J) = Query)),
     Post => A (Find_Array'Result) = Query;
end Ex1;
---
package body Ex1 is

   function Find_Array (A : Arr; Query : Natural) return Extended_Index is
      Result : Extended_Index := 0;
   begin
      for Cur in Index range A'Range loop
         if A (Cur) = Query then
            Result := Cur;
            exit;
         end if;
         pragma Assert (for all J in Index range A'First .. Cur =>
                          (A (J) /= Query));
      end loop;
      return Result;
   end Find_Array;
end Ex1;

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

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

	* sem_ch3.adb (Process_Range_In_Decl): If the range is part of a
	quantified expression, the insertion point for range checks will be
	arbitrarily far in the tree.
	* sem_ch5.adb (One_Bound): Use Insert_Actions for the declaration of
	the temporary that holds the value of the bounds.
	* sem_res.adb (Resolve_Quantified_Expressions): Disable expansion of
	condition until the full expression is expanded.

Patch

Index: sem_ch3.adb
===================================================================
--- sem_ch3.adb	(revision 165953)
+++ sem_ch3.adb	(working copy)
@@ -17627,10 +17627,10 @@  package body Sem_Ch3 is
       Check_List  : List_Id := Empty_List;
       R_Check_Off : Boolean := False)
    is
-      Lo, Hi    : Node_Id;
-      R_Checks  : Check_Result;
-      Type_Decl : Node_Id;
-      Def_Id    : Entity_Id;
+      Lo, Hi      : Node_Id;
+      R_Checks    : Check_Result;
+      Insert_Node : Node_Id;
+      Def_Id      : Entity_Id;
 
    begin
       Analyze_And_Resolve (R, Base_Type (T));
@@ -17738,32 +17738,43 @@  package body Sem_Ch3 is
             if not R_Check_Off then
                R_Checks := Get_Range_Checks (R, T);
 
-               --  Look up tree to find an appropriate insertion point.
-               --  This seems really junk code, and very brittle, couldn't
-               --  we just use an insert actions call of some kind ???
-
-               Type_Decl := Parent (R);
-               while Present (Type_Decl) and then not
-                 (Nkind_In (Type_Decl, N_Full_Type_Declaration,
-                                       N_Subtype_Declaration,
-                                       N_Loop_Statement,
-                                       N_Task_Type_Declaration)
-                    or else
-                  Nkind_In (Type_Decl, N_Single_Task_Declaration,
-                                       N_Protected_Type_Declaration,
-                                       N_Single_Protected_Declaration))
-               loop
-                  Type_Decl := Parent (Type_Decl);
+               --  Look up tree to find an appropriate insertion point. We
+               --  can't just use insert_actions because later processing
+               --  depends on the insertion node. Prior to Ada2012 the
+               --  insertion point could only be a declaration or a loop, but
+               --  quantified expressions can appear within any context in an
+               --  expression, and the insertion point can be any statement,
+               --  pragma, or declaration.
+
+               Insert_Node := Parent (R);
+               while Present (Insert_Node) loop
+                  exit when
+                    Nkind (Insert_Node) in N_Declaration
+                    and then
+                      not Nkind_In
+                        (Insert_Node, N_Component_Declaration,
+                                      N_Loop_Parameter_Specification,
+                                      N_Function_Specification,
+                                      N_Procedure_Specification);
+
+                  exit when Nkind (Insert_Node) in N_Later_Decl_Item
+                    or else Nkind (Insert_Node) in
+                              N_Statement_Other_Than_Procedure_Call
+                    or else Nkind_In (Insert_Node, N_Procedure_Call_Statement,
+                                                   N_Pragma);
+
+                  Insert_Node := Parent (Insert_Node);
                end loop;
 
                --  Why would Type_Decl not be present???  Without this test,
                --  short regression tests fail.
 
-               if Present (Type_Decl) then
+               if Present (Insert_Node) then
 
-                  --  Case of loop statement (more comments ???)
+                  --  Case of loop statement. Verify that the range is part
+                  --  of the subtype indication of the iteration scheme.
 
-                  if Nkind (Type_Decl) = N_Loop_Statement then
+                  if Nkind (Insert_Node) = N_Loop_Statement then
                      declare
                         Indic : Node_Id;
 
@@ -17780,18 +17791,20 @@  package body Sem_Ch3 is
 
                            Insert_Range_Checks
                              (R_Checks,
-                              Type_Decl,
+                              Insert_Node,
                               Def_Id,
-                              Sloc (Type_Decl),
+                              Sloc (Insert_Node),
                               R,
                               Do_Before => True);
                         end if;
                      end;
 
-                  --  All other cases (more comments ???)
+                  --  Insertion before a declaration. If the declaration
+                  --  includes discriminants, the list of applicable checks
+                  --  is given by the caller.
 
-                  else
-                     Def_Id := Defining_Identifier (Type_Decl);
+                  elsif Nkind (Insert_Node) in N_Declaration then
+                     Def_Id := Defining_Identifier (Insert_Node);
 
                      if (Ekind (Def_Id) = E_Record_Type
                           and then Depends_On_Discriminant (R))
@@ -17800,18 +17813,29 @@  package body Sem_Ch3 is
                           and then Has_Discriminants (Def_Id))
                      then
                         Append_Range_Checks
-                          (R_Checks, Check_List, Def_Id, Sloc (Type_Decl), R);
+                          (R_Checks,
+                            Check_List, Def_Id, Sloc (Insert_Node), R);
 
                      else
                         Insert_Range_Checks
-                          (R_Checks, Type_Decl, Def_Id, Sloc (Type_Decl), R);
+                          (R_Checks,
+                            Insert_Node, Def_Id, Sloc (Insert_Node), R);
 
                      end if;
+
+                  --  Insertion before a statement. Range appears in the
+                  --  context of a quantified expression. Insertion will
+                  --  take place when expression is expanded.
+
+                  else
+                     null;
                   end if;
                end if;
             end if;
          end if;
 
+      --  Case of other than an explicit N_Range node
+
       elsif Expander_Active then
          Get_Index_Bounds (R, Lo, Hi);
          Force_Evaluation (Lo);
Index: sem_ch5.adb
===================================================================
--- sem_ch5.adb	(revision 165944)
+++ sem_ch5.adb	(working copy)
@@ -1538,8 +1538,11 @@  package body Sem_Ch5 is
                    Object_Definition   => New_Occurrence_Of (Typ, Loc),
                    Expression          => Relocate_Node (Original_Bound));
 
-               Insert_Before (Parent (N), Decl);
-               Analyze (Decl);
+               --  Insert declaration at proper place. If loop comes from an
+               --  enclosing quantified expression, the insertion point is
+               --  arbitrarily far up in the tree.
+
+               Insert_Action (Parent (N), Decl);
                Rewrite (Original_Bound, New_Occurrence_Of (Id, Loc));
                return Expression (Decl);
             end if;
Index: sem_res.adb
===================================================================
--- sem_res.adb	(revision 165950)
+++ sem_res.adb	(working copy)
@@ -7809,9 +7809,13 @@  package body Sem_Res is
    procedure Resolve_Quantified_Expression (N : Node_Id; Typ : Entity_Id) is
    begin
       --  The loop structure is already resolved during its analysis, only the
-      --  resolution of the condition needs to be done.
+      --  resolution of the condition needs to be done. Expansion is disabled
+      --  so that checks and other generated code are inserted in the tree
+      --  after expression has been rewritten as a loop.
 
+      Expander_Mode_Save_And_Set (False);
       Resolve (Condition (N), Typ);
+      Expander_Mode_Restore;
    end Resolve_Quantified_Expression;
 
    -------------------