Patchwork [Ada] Attribute Update

login
register
mail settings
Submitter Arnaud Charlet
Date Dec. 5, 2012, 11:06 a.m.
Message ID <20121205110649.GA22439@adacore.com>
Download mbox | patch
Permalink /patch/203852/
State New
Headers show

Comments

Arnaud Charlet - Dec. 5, 2012, 11:06 a.m.
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.

Patch

Index: exp_attr.adb
===================================================================
--- exp_attr.adb	(revision 194190)
+++ exp_attr.adb	(working copy)
@@ -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 --
    -------------------
Index: par-ch4.adb
===================================================================
--- par-ch4.adb	(revision 194204)
+++ par-ch4.adb	(working copy)
@@ -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;
Index: sem_attr.adb
===================================================================
--- sem_attr.adb	(revision 194203)
+++ sem_attr.adb	(working copy)
@@ -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 --
       ---------------
Index: snames.ads-tmpl
===================================================================
--- snames.ads-tmpl	(revision 194203)
+++ snames.ads-tmpl	(working copy)
@@ -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,