-- --
-- B o d y --
-- --
--- Copyright (C) 1992-2018, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2020, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
with Atree; use Atree;
with Checks; use Checks;
with Einfo; use Einfo;
+with Exp_Attr;
with Exp_Ch4;
with Exp_Ch5; use Exp_Ch5;
with Exp_Dbug; use Exp_Dbug;
with Nmake; use Nmake;
with Rtsfind; use Rtsfind;
with Sem; use Sem;
-with Sem_Eval; use Sem_Eval;
+with Sem_Ch8; use Sem_Ch8;
with Sem_Prag; use Sem_Prag;
with Sem_Res; use Sem_Res;
with Sem_Util; use Sem_Util;
-----------------------
procedure Expand_SPARK_N_Attribute_Reference (N : Node_Id);
- -- Replace occurrences of System'To_Address by calls to
- -- System.Storage_Elements.To_Address
+ -- Perform attribute-reference-specific expansion
+
+ procedure Expand_SPARK_N_Delta_Aggregate (N : Node_Id);
+ -- Perform delta-aggregate-specific expansion
procedure Expand_SPARK_N_Freeze_Type (E : Entity_Id);
-- Build the DIC procedure of a type when needed, if not already done
- procedure Expand_SPARK_N_Indexed_Component (N : Node_Id);
- -- Insert explicit dereference if required
-
procedure Expand_SPARK_N_Loop_Statement (N : Node_Id);
- -- Perform loop statement-specific expansion
+ -- Perform loop-statement-specific expansion
procedure Expand_SPARK_N_Object_Declaration (N : Node_Id);
-- Perform object-declaration-specific expansion
procedure Expand_SPARK_N_Op_Ne (N : Node_Id);
-- Rewrite operator /= based on operator = when defined explicitly
- procedure Expand_SPARK_N_Selected_Component (N : Node_Id);
- -- Insert explicit dereference if required
+ procedure Expand_SPARK_Delta_Or_Update (Typ : Entity_Id; Aggr : Node_Id);
+ -- Common expansion for attribute Update and delta aggregates
------------------
-- Expand_SPARK --
when N_Attribute_Reference =>
Expand_SPARK_N_Attribute_Reference (N);
+ when N_Delta_Aggregate =>
+ Expand_SPARK_N_Delta_Aggregate (N);
+
when N_Expanded_Name
| N_Identifier
=>
Expand_SPARK_N_Freeze_Type (Entity (N));
end if;
- when N_Indexed_Component =>
- Expand_SPARK_N_Indexed_Component (N);
-
- when N_Selected_Component =>
- Expand_SPARK_N_Selected_Component (N);
-
-- In SPARK mode, no other constructs require expansion
when others =>
end case;
end Expand_SPARK;
+ ----------------------------------
+ -- Expand_SPARK_Delta_Or_Update --
+ ----------------------------------
+
+ procedure Expand_SPARK_Delta_Or_Update
+ (Typ : Entity_Id;
+ Aggr : Node_Id)
+ is
+ Assoc : Node_Id;
+ Comp : Node_Id;
+ Comp_Id : Entity_Id;
+ Comp_Type : Entity_Id;
+ Expr : Node_Id;
+ Index : Node_Id;
+ Index_Typ : Entity_Id;
+ New_Assoc : Node_Id;
+
+ begin
+ -- Apply scalar range checks on the updated components, if needed
+
+ if Is_Array_Type (Typ) then
+
+ -- Multidimensional arrays
+
+ if Present (Next_Index (First_Index (Typ))) then
+ Assoc := First (Component_Associations (Aggr));
+
+ while Present (Assoc) loop
+ Expr := Expression (Assoc);
+ Comp_Type := Component_Type (Typ);
+
+ if Is_Scalar_Type (Comp_Type) then
+ Apply_Scalar_Range_Check (Expr, Comp_Type);
+ end if;
+
+ -- The current association contains a sequence of indexes
+ -- denoting an element of a multidimensional array:
+ --
+ -- (Index_1, ..., Index_N)
+
+ Expr := First (Choices (Assoc));
+
+ pragma Assert (Nkind (Aggr) = N_Aggregate);
+
+ while Present (Expr) loop
+ Index := First (Expressions (Expr));
+ Index_Typ := First_Index (Typ);
+
+ while Present (Index_Typ) loop
+ Apply_Scalar_Range_Check (Index, Etype (Index_Typ));
+ Next (Index);
+ Next_Index (Index_Typ);
+ end loop;
+
+ Next (Expr);
+ end loop;
+
+ Next (Assoc);
+ end loop;
+
+ -- One-dimensional arrays
+
+ else
+ Assoc := First (Component_Associations (Aggr));
+
+ while Present (Assoc) loop
+ Expr := Expression (Assoc);
+ Comp_Type := Component_Type (Typ);
+
+ -- Analyze expression of the iterated_component_association
+ -- with its index parameter in scope.
+
+ if Nkind (Assoc) = N_Iterated_Component_Association then
+ Push_Scope (Scope (Defining_Identifier (Assoc)));
+ Enter_Name (Defining_Identifier (Assoc));
+ Analyze_And_Resolve (Expr, Comp_Type);
+ end if;
+
+ if Is_Scalar_Type (Comp_Type) then
+ Apply_Scalar_Range_Check (Expr, Comp_Type);
+ end if;
+
+ -- Restore scope of the iterated_component_association
+
+ if Nkind (Assoc) = N_Iterated_Component_Association then
+ End_Scope;
+ end if;
+
+ Index := First (Choice_List (Assoc));
+ Index_Typ := First_Index (Typ);
+
+ while Present (Index) loop
+ -- If the index denotes a range of elements or a constrained
+ -- subtype indication, then their low and high bounds
+ -- already have range checks applied.
+
+ if Nkind (Index) in N_Range | N_Subtype_Indication then
+ null;
+
+ -- Otherwise the index denotes a single expression where
+ -- range checks need to be applied or a subtype name
+ -- (without range constraints) where applying checks is
+ -- harmless.
+ --
+ -- In delta_aggregate and Update attribute on array the
+ -- others_choice is not allowed.
+
+ else pragma Assert (Nkind (Index) in N_Subexpr);
+ Apply_Scalar_Range_Check (Index, Etype (Index_Typ));
+ end if;
+
+ Next (Index);
+ end loop;
+
+ Next (Assoc);
+ end loop;
+ end if;
+
+ else pragma Assert (Is_Record_Type (Typ));
+
+ -- If the aggregate has multiple component choices, e.g.:
+ --
+ -- X'Update (A | B | C => 123)
+ --
+ -- then each component might be of a different type and might or
+ -- might not require a range check. We first rewrite associations
+ -- into single-component choices, e.g.:
+ --
+ -- X'Update (A => 123, B => 123, C => 123)
+ --
+ -- and then apply range checks to individual copies of the
+ -- expressions. We do the same for delta aggregates, accordingly.
+
+ -- Iterate over associations of the original aggregate
+
+ Assoc := First (Component_Associations (Aggr));
+
+ -- Rewrite into a new aggregate and decorate
+
+ case Nkind (Aggr) is
+ when N_Aggregate =>
+ Rewrite
+ (Aggr,
+ Make_Aggregate
+ (Sloc => Sloc (Aggr),
+ Component_Associations => New_List));
+
+ when N_Delta_Aggregate =>
+ Rewrite
+ (Aggr,
+ Make_Delta_Aggregate
+ (Sloc => Sloc (Aggr),
+ Expression => Expression (Aggr),
+ Component_Associations => New_List));
+
+ when others =>
+ raise Program_Error;
+ end case;
+
+ Set_Etype (Aggr, Typ);
+
+ -- Populate the new aggregate with component associations
+
+ while Present (Assoc) loop
+ Expr := Expression (Assoc);
+ Comp := First (Choices (Assoc));
+
+ while Present (Comp) loop
+ Comp_Id := Entity (Comp);
+ Comp_Type := Etype (Comp_Id);
+
+ New_Assoc :=
+ Make_Component_Association
+ (Sloc => Sloc (Assoc),
+ Choices =>
+ New_List
+ (New_Occurrence_Of (Comp_Id, Sloc (Comp))),
+ Expression => New_Copy_Tree (Expr));
+
+ -- New association must be attached to the aggregate before we
+ -- analyze it.
+
+ Append (New_Assoc, Component_Associations (Aggr));
+
+ Analyze_And_Resolve (Expression (New_Assoc), Comp_Type);
+
+ if Is_Scalar_Type (Comp_Type) then
+ Apply_Scalar_Range_Check
+ (Expression (New_Assoc), Comp_Type);
+ end if;
+
+ Next (Comp);
+ end loop;
+
+ Next (Assoc);
+ end loop;
+ end if;
+ end Expand_SPARK_Delta_Or_Update;
+
--------------------------------
-- Expand_SPARK_N_Freeze_Type --
--------------------------------
Aname : constant Name_Id := Attribute_Name (N);
Attr_Id : constant Attribute_Id := Get_Attribute_Id (Aname);
Loc : constant Source_Ptr := Sloc (N);
+ Pref : constant Node_Id := Prefix (N);
Typ : constant Entity_Id := Etype (N);
Expr : Node_Id;
Parameter_Associations => New_List (Expr)));
Analyze_And_Resolve (N, Typ);
+ elsif Attr_Id = Attribute_Object_Size
+ or else Attr_Id = Attribute_Size
+ or else Attr_Id = Attribute_Value_Size
+ or else Attr_Id = Attribute_VADS_Size
+ then
+ Exp_Attr.Expand_Size_Attribute (N);
+
-- For attributes which return Universal_Integer, introduce a conversion
-- to the expected type with the appropriate check flags set.
or else Attr_Id = Attribute_Pos
or else Attr_Id = Attribute_Position
or else Attr_Id = Attribute_Range_Length
- or else Attr_Id = Attribute_Object_Size
- or else Attr_Id = Attribute_Size
- or else Attr_Id = Attribute_Value_Size
- or else Attr_Id = Attribute_VADS_Size
or else Attr_Id = Attribute_Aft
or else Attr_Id = Attribute_Max_Alignment_For_Allocation
then
-- flag as the compiler assumes attributes always fit in this type.
-- Since in SPARK_Mode we do not take Storage_Error into account, we
-- cannot make this assumption and need to produce a check.
- -- ??? It should be enough to add this check for attributes 'Length
- -- and 'Range_Length when the type is as big as Long_Long_Integer.
+ -- ??? It should be enough to add this check for attributes
+ -- 'Length, 'Range_Length and 'Pos when the type is as big
+ -- as Long_Long_Integer.
declare
- Typ : Entity_Id := Empty;
+ Typ : Entity_Id;
begin
- if Attr_Id = Attribute_Range_Length then
+ if Attr_Id = Attribute_Range_Length
+ or else Attr_Id = Attribute_Pos
+ then
Typ := Etype (Prefix (N));
elsif Attr_Id = Attribute_Length then
- Typ := Etype (Prefix (N));
-
- declare
- Indx : Node_Id;
- J : Int;
-
- begin
- if Is_Access_Type (Typ) then
- Typ := Designated_Type (Typ);
- end if;
+ Typ := Get_Index_Subtype (N);
- if No (Expressions (N)) then
- J := 1;
- else
- J := UI_To_Int (Expr_Value (First (Expressions (N))));
- end if;
-
- Indx := First_Index (Typ);
- while J > 1 loop
- Next_Index (Indx);
- J := J - 1;
- end loop;
-
- Typ := Etype (Indx);
- end;
+ else
+ Typ := Empty;
end if;
Apply_Universal_Integer_Attribute_Checks (N);
if Present (Typ)
and then RM_Size (Typ) = RM_Size (Standard_Long_Long_Integer)
then
+ -- ??? This should rather be a range check, but this would
+ -- crash GNATprove which somehow recovers the proper kind
+ -- of check anyway.
Set_Do_Overflow_Check (N);
end if;
end;
+
+ elsif Attr_Id = Attribute_Constrained then
+
+ -- If the prefix is an access to object, the attribute applies to
+ -- the designated object, so rewrite with an explicit dereference.
+
+ if Is_Access_Type (Etype (Pref))
+ and then
+ (not Is_Entity_Name (Pref) or else Is_Object (Entity (Pref)))
+ then
+ Rewrite (Pref,
+ Make_Explicit_Dereference (Loc, Relocate_Node (Pref)));
+ Analyze_And_Resolve (N, Standard_Boolean);
+ end if;
+
+ elsif Attr_Id = Attribute_Update then
+ Expand_SPARK_Delta_Or_Update (Typ, First (Expressions (N)));
end if;
end Expand_SPARK_N_Attribute_Reference;
+ ------------------------------------
+ -- Expand_SPARK_N_Delta_Aggregate --
+ ------------------------------------
+
+ procedure Expand_SPARK_N_Delta_Aggregate (N : Node_Id) is
+ begin
+ Expand_SPARK_Delta_Or_Update (Etype (N), N);
+ end Expand_SPARK_N_Delta_Aggregate;
+
-----------------------------------
-- Expand_SPARK_N_Loop_Statement --
-----------------------------------
end if;
end Expand_SPARK_N_Loop_Statement;
- --------------------------------------
- -- Expand_SPARK_N_Indexed_Component --
- --------------------------------------
-
- procedure Expand_SPARK_N_Indexed_Component (N : Node_Id) is
- Pref : constant Node_Id := Prefix (N);
- Typ : constant Entity_Id := Etype (Pref);
-
- begin
- if Is_Access_Type (Typ) then
- Insert_Explicit_Dereference (Pref);
- Analyze_And_Resolve (Pref, Designated_Type (Typ));
- end if;
- end Expand_SPARK_N_Indexed_Component;
-
---------------------------------------
-- Expand_SPARK_N_Object_Declaration --
---------------------------------------
begin
-- Replace a reference to a renaming with the actual renamed object
- if Ekind (Obj_Id) in Object_Kind then
+ if Is_Object (Obj_Id) then
Ren := Renamed_Object (Obj_Id);
if Present (Ren) then
end if;
end Expand_SPARK_Potential_Renaming;
- ---------------------------------------
- -- Expand_SPARK_N_Selected_Component --
- ---------------------------------------
-
- procedure Expand_SPARK_N_Selected_Component (N : Node_Id) is
- Pref : constant Node_Id := Prefix (N);
- Typ : constant Entity_Id := Underlying_Type (Etype (Pref));
-
- begin
- if Present (Typ) and then Is_Access_Type (Typ) then
-
- -- First set prefix type to proper access type, in case it currently
- -- has a private (non-access) view of this type.
-
- Set_Etype (Pref, Typ);
-
- Insert_Explicit_Dereference (Pref);
- Analyze_And_Resolve (Pref, Designated_Type (Typ));
-
- if Ekind (Etype (Pref)) = E_Private_Subtype
- and then Is_For_Access_Subtype (Etype (Pref))
- then
- Set_Etype (Pref, Base_Type (Etype (Pref)));
- end if;
- end if;
- end Expand_SPARK_N_Selected_Component;
-
end Exp_SPARK;
projects / gcc.git / blobdiff