Following up on the previous change, we now move all the formal
verification expansion in a separate exp_alfa.ad? file. Previous exp_*_light
change is "reverted/canceled" at the same time (not shown here for convenience).
Instead of the full expansion targetting code generation, a light expansion
now used in formal verification mode. Light expansion has three main
objectives:
1. Perform limited expansion to explicit some Ada rules and constructs
2. Facilitate treatment for the formal verification back-end
3. Avoid the introduction of low-level code that is difficult to analyze
formally, as typically done in the full expansion for high-level
constructs (tasking, dispatching)
Also remove special exits from full expansion that were previously needed.
Tested on x86_64-pc-linux-gnu, committed on trunk
2011-08-30 Yannick Moy <m...@adacore.com>
* exp_aggr.adb, exp_ch11.adb, exp_prag.adb: Remove early exit during
expansion in Alfa mode.
* exp_ch6.adb, exp_ch6.ads (Expand_Actuals): Make subprogram public
* exp_alfa.adb, exp_alfa.ads: New package defining light expansion for
Alfa mode.
* gnat1drv.adb (Adjust_Global_Switches): Update Comment.
* sem_res.adb: Ditto.
Index: exp_prag.adb
===================================================================
--- exp_prag.adb (revision 178316)
+++ exp_prag.adb (working copy)
@@ -321,15 +321,6 @@
-- be an explicit conditional in the source, not an implicit if, so we
-- do not call Make_Implicit_If_Statement.
- -- In formal verification mode, we keep the pragma check in the code,
- -- and its enclosed expression is not expanded. This requires that no
- -- transient scope is introduced for pragma check in this mode in
- -- Exp_Ch7.Establish_Transient_Scope.
-
- if ALFA_Mode then
- return;
- end if;
-
-- Case where we generate a direct raise
if ((Debug_Flag_Dot_G
Index: exp_alfa.adb
===================================================================
--- exp_alfa.adb (revision 0)
+++ exp_alfa.adb (revision 0)
@@ -0,0 +1,270 @@
+------------------------------------------------------------------------------
+-- --
+-- GNAT COMPILER COMPONENTS --
+-- --
+-- E X P _ A L F A --
+-- --
+-- B o d y --
+-- --
+-- Copyright (C) 2011, 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- --
+-- ware Foundation; either version 3, or (at your option) any later ver- --
+-- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
+-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
+-- or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License --
+-- for more details. You should have received a copy of the GNU General --
+-- Public License distributed with GNAT; see file COPYING3. If not, go to --
+-- http://www.gnu.org/licenses for a complete copy of the license. --
+-- --
+-- GNAT was originally developed by the GNAT team at New York University. --
+-- Extensive contributions were provided by Ada Core Technologies Inc. --
+-- --
+------------------------------------------------------------------------------
+
+with Atree; use Atree;
+with Einfo; use Einfo;
+with Exp_Attr; use Exp_Attr;
+with Exp_Ch6; use Exp_Ch6;
+with Exp_Dbug; use Exp_Dbug;
+with Rtsfind; use Rtsfind;
+with Sem_Aux; use Sem_Aux;
+with Sem_Res; use Sem_Res;
+with Sinfo; use Sinfo;
+with Snames; use Snames;
+with Stand; use Stand;
+with Tbuild; use Tbuild;
+
+package body Exp_Alfa is
+
+ -----------------------
+ -- Local Subprograms --
+ -----------------------
+
+ procedure Expand_Alfa_Call (N : Node_Id);
+ -- This procedure contains common processing for function and procedure
+ -- calls:
+ -- * expansion of actuals to introduce necessary temporaries
+ -- * replacement of renaming by subprogram renamed
+
+ procedure Expand_Alfa_N_Attribute_Reference (N : Node_Id);
+ -- Expand attributes 'Old and 'Result only
+
+ procedure Expand_Alfa_N_Package_Declaration (N : Node_Id);
+ -- Fully qualify names of enclosed entities
+
+ procedure Expand_Alfa_N_Simple_Return_Statement (N : Node_Id);
+ -- Insert conversion on function return if necessary
+
+ procedure Expand_Alfa_N_Subprogram_Body (N : Node_Id);
+ -- Fully qualify names of enclosed entities
+
+ procedure Expand_Alfa_Simple_Function_Return (N : Node_Id);
+ -- Expand simple return from function
+
+ -----------------
+ -- Expand_Alfa --
+ -----------------
+
+ procedure Expand_Alfa (N : Node_Id) is
+ begin
+ case Nkind (N) is
+
+ when N_Package_Declaration =>
+ Expand_Alfa_N_Package_Declaration (N);
+
+ when N_Simple_Return_Statement =>
+ Expand_Alfa_N_Simple_Return_Statement (N);
+
+ when N_Subprogram_Body =>
+ Expand_Alfa_N_Subprogram_Body (N);
+
+ when N_Function_Call |
+ N_Procedure_Call_Statement =>
+ Expand_Alfa_Call (N);
+
+ when N_Attribute_Reference =>
+ Expand_Alfa_N_Attribute_Reference (N);
+
+ when others =>
+ null;
+
+ end case;
+ end Expand_Alfa;
+
+ ----------------------
+ -- Expand_Alfa_Call --
+ ----------------------
+
+ procedure Expand_Alfa_Call (N : Node_Id) is
+ Call_Node : constant Node_Id := N;
+ Parent_Subp : Entity_Id;
+ Subp : Entity_Id;
+
+ begin
+ -- Ignore if previous error
+
+ if Nkind (Call_Node) in N_Has_Etype
+ and then Etype (Call_Node) = Any_Type
+ then
+ return;
+ end if;
+
+ -- Call using access to subprogram with explicit dereference
+
+ if Nkind (Name (Call_Node)) = N_Explicit_Dereference then
+ Subp := Etype (Name (Call_Node));
+ Parent_Subp := Empty;
+
+ -- Case of call to simple entry, where the Name is a selected component
+ -- whose prefix is the task, and whose selector name is the entry name
+
+ elsif Nkind (Name (Call_Node)) = N_Selected_Component then
+ Subp := Entity (Selector_Name (Name (Call_Node)));
+ Parent_Subp := Empty;
+
+ -- Case of call to member of entry family, where Name is an indexed
+ -- component, with the prefix being a selected component giving the
+ -- task and entry family name, and the index being the entry index.
+
+ elsif Nkind (Name (Call_Node)) = N_Indexed_Component then
+ Subp := Entity (Selector_Name (Prefix (Name (Call_Node))));
+ Parent_Subp := Empty;
+
+ -- Normal case
+
+ else
+ Subp := Entity (Name (Call_Node));
+ Parent_Subp := Alias (Subp);
+ end if;
+
+ -- Various expansion activities for actuals are carried out
+
+ Expand_Actuals (N, Subp);
+
+ -- If the subprogram is a renaming, replace it in the call with the name
+ -- of the actual subprogram being called.
+
+ if Present (Parent_Subp) then
+ Parent_Subp := Ultimate_Alias (Parent_Subp);
+
+ -- The below setting of Entity is suspect, see F109-018 discussion???
+
+ Set_Entity (Name (Call_Node), Parent_Subp);
+ end if;
+
+ end Expand_Alfa_Call;
+
+ ---------------------------------------
+ -- Expand_Alfa_N_Attribute_Reference --
+ ---------------------------------------
+
+ procedure Expand_Alfa_N_Attribute_Reference (N : Node_Id) is
+ Id : constant Attribute_Id := Get_Attribute_Id (Attribute_Name (N));
+
+ begin
+ case Id is
+ when Attribute_Old |
+ Attribute_Result =>
+ Expand_N_Attribute_Reference (N);
+
+ when others =>
+ null;
+ end case;
+ end Expand_Alfa_N_Attribute_Reference;
+
+ ---------------------------------------
+ -- Expand_Alfa_N_Package_Declaration --
+ ---------------------------------------
+
+ procedure Expand_Alfa_N_Package_Declaration (N : Node_Id) is
+ begin
+ Qualify_Entity_Names (N);
+ end Expand_Alfa_N_Package_Declaration;
+
+ -------------------------------------------
+ -- Expand_Alfa_N_Simple_Return_Statement --
+ -------------------------------------------
+
+ procedure Expand_Alfa_N_Simple_Return_Statement (N : Node_Id) is
+ begin
+ -- Defend against previous errors (i.e. the return statement calls a
+ -- function that is not available in configurable runtime).
+
+ if Present (Expression (N))
+ and then Nkind (Expression (N)) = N_Empty
+ then
+ return;
+ end if;
+
+ -- Distinguish the function and non-function cases:
+
+ case Ekind (Return_Applies_To (Return_Statement_Entity (N))) is
+
+ when E_Function |
+ E_Generic_Function =>
+ Expand_Alfa_Simple_Function_Return (N);
+
+ when E_Procedure |
+ E_Generic_Procedure |
+ E_Entry |
+ E_Entry_Family |
+ E_Return_Statement =>
+ -- Expand_Non_Function_Return (N);
+ null;
+
+ when others =>
+ raise Program_Error;
+ end case;
+
+ exception
+ when RE_Not_Available =>
+ return;
+ end Expand_Alfa_N_Simple_Return_Statement;
+
+ -----------------------------------
+ -- Expand_Alfa_N_Subprogram_Body --
+ -----------------------------------
+
+ procedure Expand_Alfa_N_Subprogram_Body (N : Node_Id) is
+ begin
+ Qualify_Entity_Names (N);
+ end Expand_Alfa_N_Subprogram_Body;
+
+ ----------------------------------------
+ -- Expand_Alfa_Simple_Function_Return --
+ ----------------------------------------
+
+ procedure Expand_Alfa_Simple_Function_Return (N : Node_Id) is
+ Scope_Id : constant Entity_Id :=
+ Return_Applies_To (Return_Statement_Entity (N));
+ -- The function we are returning from
+
+ R_Type : constant Entity_Id := Etype (Scope_Id);
+ -- The result type of the function
+
+ Exp : constant Node_Id := Expression (N);
+ pragma Assert (Present (Exp));
+
+ Exptyp : constant Entity_Id := Etype (Exp);
+ -- The type of the expression (not necessarily the same as R_Type)
+
+ begin
+ -- Check the result expression of a scalar function against the subtype
+ -- of the function by inserting a conversion. This conversion must
+ -- eventually be performed for other classes of types, but for now it's
+ -- only done for scalars.
+ -- ???
+
+ if Is_Scalar_Type (Exptyp) then
+ Rewrite (Exp, Convert_To (R_Type, Exp));
+
+ -- The expression is resolved to ensure that the conversion gets
+ -- expanded to generate a possible constraint check.
+
+ Analyze_And_Resolve (Exp, R_Type);
+ end if;
+ end Expand_Alfa_Simple_Function_Return;
+
+end Exp_Alfa;
Index: exp_alfa.ads
===================================================================
--- exp_alfa.ads (revision 0)
+++ exp_alfa.ads (revision 0)
@@ -0,0 +1,52 @@
+------------------------------------------------------------------------------
+-- --
+-- GNAT COMPILER COMPONENTS --
+-- --
+-- E X P _ A L F A --
+-- --
+-- S p e c --
+-- --
+-- Copyright (C) 2011, 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- --
+-- ware Foundation; either version 3, or (at your option) any later ver- --
+-- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
+-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
+-- or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License --
+-- for more details. You should have received a copy of the GNU General --
+-- Public License distributed with GNAT; see file COPYING3. If not, go to --
+-- http://www.gnu.org/licenses for a complete copy of the license. --
+-- --
+-- GNAT was originally developed by the GNAT team at New York University. --
+-- Extensive contributions were provided by Ada Core Technologies Inc. --
+-- --
+------------------------------------------------------------------------------
+
+-- This package implements a light expansion which is used in formal
+-- verification mode. Instead of a complete expansion of nodes for code
+-- generation, this Alfa expansion targets generation of intermediate code
+-- for formal verification.
+
+-- Expand_Alfa is called directly by Expander.Expand.
+
+-- Alfa expansion has three main objectives:
+
+-- 1. Perform limited expansion to explicit some Ada rules and constructs
+-- (translate 'Old and 'Result, replace renamings by renamed, insert
+-- conversions, expand actuals in calls to introduce temporaries)
+
+-- 2. Facilitate treatment for the formal verification back-end (fully
+-- qualify names)
+
+-- 3. Avoid the introduction of low-level code that is difficult to analyze
+-- formally, as typically done in the full expansion for high-level
+-- constructs (tasking, dispatching)
+
+with Types; use Types;
+
+package Exp_Alfa is
+
+ procedure Expand_Alfa (N : Node_Id);
+
+end Exp_Alfa;
Index: sem_res.adb
===================================================================
--- sem_res.adb (revision 178314)
+++ sem_res.adb (working copy)
@@ -8094,8 +8094,8 @@
Resolve (Condition (N), Typ);
Expander_Mode_Restore;
- -- In ALFA_Mode, no magic needed, we just resolve the underlying nodes
- -- But why is this special handling for ALFA_Mode required ???
+ -- In ALFA mode, we need expansion in order to introduce properly the
+ -- necessary transient scopes.
else
Resolve (Condition (N), Typ);
Index: expander.adb
===================================================================
--- expander.adb (revision 178316)
+++ expander.adb (working copy)
@@ -27,6 +27,7 @@
with Debug_A; use Debug_A;
with Errout; use Errout;
with Exp_Aggr; use Exp_Aggr;
+with Exp_Alfa; use Exp_Alfa;
with Exp_Attr; use Exp_Attr;
with Exp_Ch2; use Exp_Ch2;
with Exp_Ch3; use Exp_Ch3;
@@ -131,8 +132,13 @@
-- routines.
begin
- case Nkind (N) is
+ if ALFA_Mode then
+ Expand_Alfa (N);
+ else
+
+ case Nkind (N) is
+
when N_Abort_Statement =>
Expand_N_Abort_Statement (N);
@@ -449,8 +455,10 @@
when others => null;
- end case;
+ end case;
+ end if;
+
exception
when RE_Not_Available =>
return;
Index: gnat1drv.adb
===================================================================
--- gnat1drv.adb (revision 178316)
+++ gnat1drv.adb (working copy)
@@ -435,8 +435,9 @@
Polling_Required := False;
- -- Set operating mode to Generate_Code to benefit from full front-end
- -- expansion (e.g. default arguments).
+ -- Set operating mode to Generate_Code, but full front-end expansion
+ -- is not desirable in ALFA mode, so a light expansion is performed
+ -- instead.
Operating_Mode := Generate_Code;
Index: exp_ch11.adb
===================================================================
--- exp_ch11.adb (revision 178316)
+++ exp_ch11.adb (working copy)
@@ -1673,7 +1673,6 @@
if VM_Target = No_VM
and then not CodePeer_Mode
- and then not ALFA_Mode
and then Exception_Mechanism = Back_End_Exceptions
then
return;
Index: exp_ch6.adb
===================================================================
--- exp_ch6.adb (revision 178316)
+++ exp_ch6.adb (working copy)
@@ -156,36 +156,6 @@
-- the values are not changed for the call, we know immediately that
-- we have an infinite recursion.
- procedure Expand_Actuals (N : Node_Id; Subp : Entity_Id);
- -- For each actual of an in-out or out parameter which is a numeric
- -- (view) conversion of the form T (A), where A denotes a variable,
- -- we insert the declaration:
- --
- -- Temp : T[ := T (A)];
- --
- -- prior to the call. Then we replace the actual with a reference to Temp,
- -- and append the assignment:
- --
- -- A := TypeA (Temp);
- --
- -- after the call. Here TypeA is the actual type of variable A. For out
- -- parameters, the initial declaration has no expression. If A is not an
- -- entity name, we generate instead:
- --
- -- Var : TypeA renames A;
- -- Temp : T := Var; -- omitting expression for out parameter.
- -- ...
- -- Var := TypeA (Temp);
- --
- -- For other in-out parameters, we emit the required constraint checks
- -- before and/or after the call.
- --
- -- For all parameter modes, actuals that denote components and slices of
- -- packed arrays are expanded into suitable temporaries.
- --
- -- For non-scalar objects that are possibly unaligned, add call by copy
- -- code (copy in for IN and IN OUT, copy out for OUT and IN OUT).
-
procedure Expand_Ctrl_Function_Call (N : Node_Id);
-- N is a function call which returns a controlled object. Transform the
-- call into a temporary which retrieves the returned object from the
Index: exp_ch6.ads
===================================================================
--- exp_ch6.ads (revision 178316)
+++ exp_ch6.ads (working copy)
@@ -37,6 +37,36 @@
procedure Expand_N_Subprogram_Body_Stub (N : Node_Id);
procedure Expand_N_Subprogram_Declaration (N : Node_Id);
+ procedure Expand_Actuals (N : Node_Id; Subp : Entity_Id);
+ -- For each actual of an in-out or out parameter which is a numeric
+ -- (view) conversion of the form T (A), where A denotes a variable,
+ -- we insert the declaration:
+ --
+ -- Temp : T[ := T (A)];
+ --
+ -- prior to the call. Then we replace the actual with a reference to Temp,
+ -- and append the assignment:
+ --
+ -- A := TypeA (Temp);
+ --
+ -- after the call. Here TypeA is the actual type of variable A. For out
+ -- parameters, the initial declaration has no expression. If A is not an
+ -- entity name, we generate instead:
+ --
+ -- Var : TypeA renames A;
+ -- Temp : T := Var; -- omitting expression for out parameter.
+ -- ...
+ -- Var := TypeA (Temp);
+ --
+ -- For other in-out parameters, we emit the required constraint checks
+ -- before and/or after the call.
+ --
+ -- For all parameter modes, actuals that denote components and slices of
+ -- packed arrays are expanded into suitable temporaries.
+ --
+ -- For non-scalar objects that are possibly unaligned, add call by copy
+ -- code (copy in for IN and IN OUT, copy out for OUT and IN OUT).
+
procedure Expand_Call (N : Node_Id);
-- This procedure contains common processing for Expand_N_Function_Call,
-- Expand_N_Procedure_Statement, and Expand_N_Entry_Call.
Index: exp_aggr.adb
===================================================================
--- exp_aggr.adb (revision 178316)
+++ exp_aggr.adb (working copy)
@@ -4664,12 +4664,6 @@
Check_Same_Aggr_Bounds (N, 1);
end if;
- -- In formal verification mode, leave the aggregate non-expanded
-
- if ALFA_Mode then
- return;
- end if;
-
-- STEP 2
-- Here we test for is packed array aggregate that we can handle at
