[Ada] Quantified expressions in pre/postconditions and other contexts
Arnaud Charlet
charlet@adacore.com
Tue Oct 26 15:01:00 GMT 2010
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.
-------------- next part --------------
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;
-------------------
More information about the Gcc-patches
mailing list