===================================================================
@@ -140,6 +140,9 @@
-- Handles expansion of Pred or Succ attributes for case of non-real
-- operand with overflow checking required.
+ procedure Expand_Update_Attribute (N : Node_Id);
+ -- Handle the expansion of attribute Update
+
function Get_Index_Subtype (N : Node_Id) return Entity_Id;
-- Used for Last, Last, and Length, when the prefix is an array type.
-- Obtains the corresponding index subtype.
@@ -5237,6 +5240,13 @@
Analyze_And_Resolve (N, Typ);
end UET_Address;
+ ------------
+ -- Update --
+ ------------
+
+ when Attribute_Update =>
+ Expand_Update_Attribute (N);
+
---------------
-- VADS_Size --
---------------
@@ -6160,6 +6170,197 @@
end if;
end Expand_Pred_Succ;
+ -----------------------------
+ -- Expand_Update_Attribute --
+ -----------------------------
+
+ procedure Expand_Update_Attribute (N : Node_Id) is
+ procedure Process_Component_Or_Element_Update
+ (Temp : Entity_Id;
+ Comp : Node_Id;
+ Expr : Node_Id;
+ Typ : Entity_Id);
+ -- Generate the statements necessary to update a single component or an
+ -- element of the prefix. The code is inserted before the attribute N.
+ -- Temp denotes the entity of the anonymous object created to reflect
+ -- the changes in values. Comp is the component/index expression to be
+ -- updated. Expr is an expression yielding the new value of Comp. Typ
+ -- is the type of the prefix of attribute Update.
+
+ procedure Process_Range_Update
+ (Temp : Entity_Id;
+ Comp : Node_Id;
+ Expr : Node_Id);
+ -- Generate the statements necessary to update a slice of the prefix.
+ -- The code is inserted before the attribute N. Temp denotes the entity
+ -- of the anonymous object created to reflect the changes in values.
+ -- Comp is range of the slice to be updated. Expr is an expression
+ -- yielding the new value of Comp.
+
+ -----------------------------------------
+ -- Process_Component_Or_Element_Update --
+ -----------------------------------------
+
+ procedure Process_Component_Or_Element_Update
+ (Temp : Entity_Id;
+ Comp : Node_Id;
+ Expr : Node_Id;
+ Typ : Entity_Id)
+ is
+ Loc : constant Source_Ptr := Sloc (Comp);
+ Exprs : List_Id;
+ LHS : Node_Id;
+
+ begin
+ -- An array element may be modified by the following relations
+ -- depending on the number of dimensions:
+
+ -- 1 => Expr -- one dimensional update
+ -- (1, ..., N) => Expr -- multi dimensional update
+
+ -- The above forms are converted in assignment statements where the
+ -- left hand side is an indexed component:
+
+ -- Temp (1) := Expr; -- one dimensional update
+ -- Temp (1, ..., N) := Expr; -- multi dimensional update
+
+ if Is_Array_Type (Typ) then
+
+ -- The index expressions of a multi dimensional array update
+ -- appear as an aggregate.
+
+ if Nkind (Comp) = N_Aggregate then
+ Exprs := New_Copy_List_Tree (Expressions (Comp));
+ else
+ Exprs := New_List (Relocate_Node (Comp));
+ end if;
+
+ LHS :=
+ Make_Indexed_Component (Loc,
+ Prefix => New_Reference_To (Temp, Loc),
+ Expressions => Exprs);
+
+ -- A record component update appears in the following form:
+
+ -- Comp => Expr
+
+ -- The above relation is transformed into an assignment statement
+ -- where the left hand side is a selected component:
+
+ -- Temp.Comp := Expr;
+
+ else pragma Assert (Is_Record_Type (Typ));
+ LHS :=
+ Make_Selected_Component (Loc,
+ Prefix => New_Reference_To (Temp, Loc),
+ Selector_Name => Relocate_Node (Comp));
+ end if;
+
+ Insert_Action (N,
+ Make_Assignment_Statement (Loc,
+ Name => LHS,
+ Expression => Relocate_Node (Expr)));
+ end Process_Component_Or_Element_Update;
+
+ --------------------------
+ -- Process_Range_Update --
+ --------------------------
+
+ procedure Process_Range_Update
+ (Temp : Entity_Id;
+ Comp : Node_Id;
+ Expr : Node_Id)
+ is
+ Loc : constant Source_Ptr := Sloc (Comp);
+ Index : Entity_Id;
+
+ begin
+ -- A range update appears as
+
+ -- (Low .. High => Expr)
+
+ -- The above construct is transformed into a loop that iterates over
+ -- the given range and modifies the corresponding array values to the
+ -- value of Expr:
+
+ -- for Index in Low .. High loop
+ -- Temp (Index) := Expr;
+ -- end loop;
+
+ Index := Make_Temporary (Loc, 'I');
+
+ Insert_Action (N,
+ Make_Loop_Statement (Loc,
+ Iteration_Scheme =>
+ Make_Iteration_Scheme (Loc,
+ Loop_Parameter_Specification =>
+ Make_Loop_Parameter_Specification (Loc,
+ Defining_Identifier => Index,
+ Discrete_Subtype_Definition => Relocate_Node (Comp))),
+
+ Statements => New_List (
+ Make_Assignment_Statement (Loc,
+ Name =>
+ Make_Indexed_Component (Loc,
+ Prefix => New_Reference_To (Temp, Loc),
+ Expressions => New_List (New_Reference_To (Index, Loc))),
+ Expression => Relocate_Node (Expr))),
+
+ End_Label => Empty));
+ end Process_Range_Update;
+
+ -- Local variables
+
+ Aggr : constant Node_Id := First (Expressions (N));
+ Loc : constant Source_Ptr := Sloc (N);
+ Pref : constant Node_Id := Prefix (N);
+ Typ : constant Entity_Id := Etype (Pref);
+ Assoc : Node_Id;
+ Comp : Node_Id;
+ Expr : Node_Id;
+ Temp : Entity_Id;
+
+ -- Start of processing for Expand_Update_Attribute
+
+ begin
+ -- Create the anonymous object that stores the value of the prefix and
+ -- reflects subsequent changes in value. Generate:
+
+ -- Temp : <type of Pref> := Pref;
+
+ Temp := Make_Temporary (Loc, 'T');
+
+ Insert_Action (N,
+ Make_Object_Declaration (Loc,
+ Defining_Identifier => Temp,
+ Object_Definition => New_Reference_To (Typ, Loc),
+ Expression => Relocate_Node (Pref)));
+
+ -- Process the update aggregate
+
+ Assoc := First (Component_Associations (Aggr));
+ while Present (Assoc) loop
+ Comp := First (Choices (Assoc));
+ Expr := Expression (Assoc);
+ while Present (Comp) loop
+ if Nkind (Comp) = N_Range then
+ Process_Range_Update (Temp, Comp, Expr);
+ else
+ Process_Component_Or_Element_Update (Temp, Comp, Expr, Typ);
+ end if;
+
+ Next (Comp);
+ end loop;
+
+ Next (Assoc);
+ end loop;
+
+ -- The attribute is replaced by a reference to the anonymous object
+
+ Rewrite (N, New_Reference_To (Temp, Loc));
+ Analyze (N);
+ end Expand_Update_Attribute;
+
-------------------
-- Find_Fat_Info --
-------------------
===================================================================
@@ -510,26 +510,36 @@
Is_Parameterless_Attribute (Get_Attribute_Id (Attr_Name))
then
Set_Expressions (Name_Node, New_List);
- Scan; -- past left paren
- loop
- declare
- Expr : constant Node_Id := P_Expression_If_OK;
+ -- Attribute Update contains an array or record association
+ -- list which provides new values for various components or
+ -- elements. The list is parsed as an aggregate.
- begin
- if Token = Tok_Arrow then
- Error_Msg_SC
- ("named parameters not permitted for attributes");
- Scan; -- past junk arrow
+ if Attr_Name = Name_Update then
+ Append (P_Aggregate, Expressions (Name_Node));
- else
- Append (Expr, Expressions (Name_Node));
- exit when not Comma_Present;
- end if;
- end;
- end loop;
+ else
+ Scan; -- past left paren
- T_Right_Paren;
+ loop
+ declare
+ Expr : constant Node_Id := P_Expression_If_OK;
+
+ begin
+ if Token = Tok_Arrow then
+ Error_Msg_SC
+ ("named parameters not permitted for attributes");
+ Scan; -- past junk arrow
+
+ else
+ Append (Expr, Expressions (Name_Node));
+ exit when not Comma_Present;
+ end if;
+ end;
+ end loop;
+
+ T_Right_Paren;
+ end if;
end if;
goto Scan_Name_Extension;
===================================================================
@@ -5516,6 +5516,164 @@
Analyze_Access_Attribute;
+ ------------
+ -- Update --
+ ------------
+
+ when Attribute_Update => Update : declare
+ Comps : Elist_Id := No_Elist;
+
+ procedure Check_Component_Reference
+ (Comp : Entity_Id;
+ Typ : Entity_Id);
+ -- Comp is a record component (possibly a discriminant) and Typ is a
+ -- record type. Determine whether Comp is a legal component of Typ.
+ -- Emit an error if Comp mentions a discriminant or is not a unique
+ -- component reference in the update aggregate.
+
+ -------------------------------
+ -- Check_Component_Reference --
+ -------------------------------
+
+ procedure Check_Component_Reference
+ (Comp : Entity_Id;
+ Typ : Entity_Id)
+ is
+ Comp_Name : constant Name_Id := Chars (Comp);
+
+ function Is_Duplicate_Component return Boolean;
+ -- Determine whether component Comp already appears in list Comps
+
+ ----------------------------
+ -- Is_Duplicate_Component --
+ ----------------------------
+
+ function Is_Duplicate_Component return Boolean is
+ Comp_Elmt : Elmt_Id;
+
+ begin
+ if Present (Comps) then
+ Comp_Elmt := First_Elmt (Comps);
+ while Present (Comp_Elmt) loop
+ if Chars (Node (Comp_Elmt)) = Comp_Name then
+ return True;
+ end if;
+
+ Next_Elmt (Comp_Elmt);
+ end loop;
+ end if;
+
+ return False;
+ end Is_Duplicate_Component;
+
+ -- Local variables
+
+ Comp_Or_Discr : Entity_Id;
+
+ -- Start of processing for Check_Component_Reference
+
+ begin
+ -- Find the discriminant or component whose name corresponds to
+ -- Comp. A simple character comparison is sufficient because all
+ -- visible names within a record type are unique.
+
+ Comp_Or_Discr := First_Entity (Typ);
+ while Present (Comp_Or_Discr) loop
+ if Chars (Comp_Or_Discr) = Comp_Name then
+ exit;
+ end if;
+
+ Comp_Or_Discr := Next_Entity (Comp_Or_Discr);
+ end loop;
+
+ -- Diagnose possible erroneous references
+
+ if Present (Comp_Or_Discr) then
+ if Ekind (Comp_Or_Discr) = E_Discriminant then
+ Error_Attr
+ ("attribute % may not modify record discriminants", Comp);
+
+ else pragma Assert (Ekind (Comp_Or_Discr) = E_Component);
+ if Is_Duplicate_Component then
+ Error_Msg_NE ("component & already updated", Comp, Comp);
+
+ -- Mark this component as processed
+
+ else
+ if No (Comps) then
+ Comps := New_Elmt_List;
+ end if;
+
+ Append_Elmt (Comp, Comps);
+ end if;
+ end if;
+
+ -- The update aggregate mentions an entity that does not belong to
+ -- the record type.
+
+ else
+ Error_Msg_NE
+ ("& is not a component of aggregate subtype", Comp, Comp);
+ end if;
+ end Check_Component_Reference;
+
+ -- Local variables
+
+ Assoc : Node_Id;
+ Comp : Node_Id;
+
+ -- Start of processing for Update
+
+ begin
+ S14_Attribute;
+ Check_E1;
+
+ if not Is_Object_Reference (P) then
+ Error_Attr_P ("prefix of attribute % must denote an object");
+
+ elsif not Is_Array_Type (P_Type)
+ and then not Is_Record_Type (P_Type)
+ then
+ Error_Attr_P ("prefix of attribute % must be a record or array");
+
+ elsif Is_Immutably_Limited_Type (P_Type) then
+ Error_Attr ("prefix of attribute % cannot be limited", N);
+
+ elsif Nkind (E1) /= N_Aggregate then
+ Error_Attr ("attribute % requires component association list", N);
+ end if;
+
+ -- Inspect the update aggregate, looking at all the associations and
+ -- choices. Perform the following checks:
+
+ -- 1) Legality of "others" in all cases
+ -- 2) Component legality for records
+
+ -- The remaining checks are performed on the expanded attribute
+
+ Assoc := First (Component_Associations (E1));
+ while Present (Assoc) loop
+ Comp := First (Choices (Assoc));
+ while Present (Comp) loop
+ if Nkind (Comp) = N_Others_Choice then
+ Error_Attr
+ ("others choice not allowed in attribute %", Comp);
+
+ elsif Is_Record_Type (P_Type) then
+ Check_Component_Reference (Comp, P_Type);
+ end if;
+
+ Next (Comp);
+ end loop;
+
+ Next (Assoc);
+ end loop;
+
+ -- The type of attribute Update is that of the prefix
+
+ Set_Etype (N, P_Type);
+ end Update;
+
---------
-- Val --
---------
@@ -8210,6 +8368,15 @@
Static := True;
end Unconstrained_Array;
+ -- Attribute Update is never static
+
+ ------------
+ -- Update --
+ ------------
+
+ when Attribute_Update =>
+ null;
+
---------------
-- VADS_Size --
---------------
===================================================================
@@ -901,6 +901,7 @@
Name_Unconstrained_Array : constant Name_Id := N + $;
Name_Universal_Literal_String : constant Name_Id := N + $; -- GNAT
Name_Unrestricted_Access : constant Name_Id := N + $; -- GNAT
+ Name_Update : constant Name_Id := N + $; -- GNAT
Name_VADS_Size : constant Name_Id := N + $; -- GNAT
Name_Val : constant Name_Id := N + $;
Name_Valid : constant Name_Id := N + $;
@@ -1512,6 +1513,7 @@
Attribute_Unconstrained_Array,
Attribute_Universal_Literal_String,
Attribute_Unrestricted_Access,
+ Attribute_Update,
Attribute_VADS_Size,
Attribute_Val,
Attribute_Valid,
This patch provides the initial implementation of attribute Update. This construct is intended for formal verification proofs. The syntax of the attribute is as follows: X'Update ( RECORD_COMPONENT_ASSOCIATION_LIST ) X'Update ( ARRAY_COMPONENT_ASSOCIATION {, ARRAY_COMPONENT_ASSOCIATION} ) X'Update ( MULTIDIMENSIONAL_ARRAY_COMPONENT_ASSOCIATION {, MULTIDIMENSIONAL_ARRAY_COMPONENT_ASSOCIATION} ) MULTIDIMENSIONAL_ARRAY_COMPONENT_ASSOCIATION ::= INDEX_EXPRESSION_LIST_LIST => EXPRESSION INDEX_EXPRESSION_LIST_LIST ::= INDEX_EXPRESSION_LIST { | INDEX_EXPRESSION_LIST} INDEX_EXPRESSION_LIST ::= (EXPRESSION {, EXPRESSION} ) The brief semantics of this attribute are as follows: The prefix of attribute Update must be a non-limited object of a record or array type. The type of the attribute is that of its prefix. The evaluation of attribute Update begins with the creation of an anonymous object of type T which is initialized to the value of the prefix. Next, components of the object are updated to new values as specified by the corresponding association_list. The attribute reference then denotes the constant view of this updated object. A record update may not modify discriminants and it is not allowed to mention components more than once. An array update modifies specified elements in the same order of their appearance in the corresponding association_list. The use of "others" in the association_lists is not allowed. ------------ -- Source -- ------------ -- main.adb with Ada.Text_IO; use Ada.Text_IO; procedure Main is type Rec is record Comp_1 : Natural; Comp_2 : Natural; end record; procedure Output_Rec (Obj : Rec) is begin Put_Line ("Comp_1:" & Obj.Comp_1'Img); Put_Line ("Comp_2:" & Obj.Comp_2'Img); end Output_Rec; Base_Obj : constant Rec := (1, 2); Obj : constant Rec := Base_Obj'Update (Comp_2 => 3); begin Output_Rec (Base_Obj); Output_Rec (Obj); end Main; ---------------------------- -- Compilation and output -- ---------------------------- $ gnatmake -q -gnatd.V main.adb $ ./main Comp_1: 1 Comp_2: 2 Comp_1: 1 Comp_2: 3 Tested on x86_64-pc-linux-gnu, committed on trunk 2012-12-05 Hristian Kirtchev <kirtchev@adacore.com> * exp_attr.adb (Expand_N_Attribute_Reference): Add processing for attribute Update. (Expand_Update_Attribute): New routine. * par-ch4.adb (P_Name): The sole expression of attribute Update is an aggregate, parse it accordingly. * sem_attr.adb (Analyze_Attribute): Verify the legality of attribute Update. (Eval_Attribute): Attribute Update does not need evaluation because it is never static. * snames.ads-tmpl: Add Name_Update to the list of special names recognized by the compiler. Add an Attribute_Id for Update.