-- --
-- S p e c --
-- --
--- Copyright (C) 2011, Free Software Foundation, Inc. --
+-- Copyright (C) 2011-2012, 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- --
------------------------------------------------------------------------------
-- 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.
+-- verification mode (Alfa_Mode = True). 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.
-- 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)
+-- conversions, expand actuals in calls to introduce temporaries, expand
+-- generics instantiations)
-- 2. Facilitate treatment for the formal verification back-end (fully
--- qualify names, set membership)
+-- qualify names, expand set membership, compute data dependences)
-- 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)
+-- To fulfill objective 1, Expand_Alfa selectively expands some constructs.
+
+-- To fulfill objective 2, the tree after Alfa expansion should be fully
+-- analyzed semantically. In particular, all expression must have their proper
+-- type, and semantic links should be set between tree nodes (partial to full
+-- view, etc.) Some kinds of nodes should be either absent, or can be ignored
+-- by the formal verification backend:
+
+-- N_Object_Renaming_Declaration: can be ignored safely
+-- N_Expression_Function: absent (rewitten)
+-- N_Expression_With_Actions: absent (not generated)
+
+-- Alfa cross-references are generated from the regular cross-references (used
+-- for browsing and code understanding) and additional references collected
+-- during semantic analysis, in particular on all dereferences. These Alfa
+-- cross-references are output in a separate section of ALI files, as
+-- described in alfa.adb. They are the basis for the computation of data
+-- dependences in the formal verification backend. This implies that all
+-- cross-references should be generated in this mode, even those that would
+-- not make sense from a user point-of-view, and that cross-references that do
+-- not lead to data dependences for subprograms can be safely ignored.
+
+-- To support the formal verification of units parameterized by data, the
+-- value of deferred constants should not be considered as a compile-time
+-- constant at program locations where the full view is not visible.
+
+-- To fulfill objective 3, Expand_Alfa does not expand features that are not
+-- formally analyzed (tasking), or for which formal analysis relies on the
+-- source level representation (dispatching, aspects, pragmas). However, these
+-- should be semantically analyzed, which sometimes requires the insertion of
+-- semantic pre-analysis, for example for subprogram contracts and pragma
+-- check/assert.
+
with Types; use Types;
package Exp_Alfa is
Actuals : List_Id;
Proc_To_Call : Entity_Id;
Except : Node_Id;
+ Stmts : List_Id;
begin
- pragma Assert (Present (Data.E_Id));
pragma Assert (Present (Data.Raised_Id));
- -- Generate:
+ if Exception_Extra_Info
+ or else (For_Library and then not Restricted_Profile)
+ then
+ if Exception_Extra_Info then
+ -- Generate:
- -- Get_Current_Excep.all
+ -- Get_Current_Excep.all
- Except :=
- Make_Function_Call (Data.Loc,
- Name =>
- Make_Explicit_Dereference (Data.Loc,
- Prefix =>
- New_Reference_To (RTE (RE_Get_Current_Excep), Data.Loc)));
+ Except :=
+ Make_Function_Call (Data.Loc,
+ Name =>
+ Make_Explicit_Dereference (Data.Loc,
+ Prefix =>
+ New_Reference_To (RTE (RE_Get_Current_Excep),
+ Data.Loc)));
+ else
+ -- Generate:
- if For_Library and not Restricted_Profile then
- Proc_To_Call := RTE (RE_Save_Library_Occurrence);
- Actuals := New_List (Except);
- else
- Proc_To_Call := RTE (RE_Save_Occurrence);
- Actuals :=
- New_List
- (New_Reference_To (Data.E_Id, Data.Loc),
+ -- null
+
+ Except := Make_Null (Data.Loc);
+ end if;
+
+ if For_Library and then not Restricted_Profile then
+ Proc_To_Call := RTE (RE_Save_Library_Occurrence);
+ Actuals := New_List (Except);
+ else
+ Proc_To_Call := RTE (RE_Save_Occurrence);
+
+ -- The dereference occurs only when Exception_Extra_Info is true,
+ -- and therefore Except is not null.
+
+ Actuals := New_List (
+ New_Reference_To (Data.E_Id, Data.Loc),
Make_Explicit_Dereference (Data.Loc, Except));
+ end if;
+
+ -- Generate:
+
+ -- when others =>
+ -- if not Raised_Id then
+ -- Raised_Id := True;
+
+ -- Save_Occurrence (E_Id, Get_Current_Excep.all.all);
+ -- or
+ -- Save_Library_Occurrence (Get_Current_Excep.all);
+ -- end if;
+
+ Stmts :=
+ New_List (
+ Make_If_Statement (Data.Loc,
+ Condition =>
+ Make_Op_Not (Data.Loc,
+ Right_Opnd => New_Reference_To (Data.Raised_Id, Data.Loc)),
+
+ Then_Statements => New_List (
+ Make_Assignment_Statement (Data.Loc,
+ Name => New_Reference_To (Data.Raised_Id, Data.Loc),
+ Expression => New_Reference_To (Standard_True, Data.Loc)),
+
+ Make_Procedure_Call_Statement (Data.Loc,
+ Name =>
+ New_Reference_To (Proc_To_Call, Data.Loc),
+ Parameter_Associations => Actuals))));
+
+ else
+ -- Generate:
+
+ -- Raised_Id := True;
+
+ Stmts := New_List (
+ Make_Assignment_Statement (Data.Loc,
+ Name => New_Reference_To (Data.Raised_Id, Data.Loc),
+ Expression => New_Reference_To (Standard_True, Data.Loc)));
end if;
-- Generate:
-- when others =>
- -- if not Raised_Id then
- -- Raised_Id := True;
-
- -- Save_Occurrence (E_Id, Get_Current_Excep.all.all);
- -- or
- -- Save_Library_Occurrence (Get_Current_Excep.all);
- -- end if;
return
Make_Exception_Handler (Data.Loc,
- Exception_Choices =>
- New_List (Make_Others_Choice (Data.Loc)),
- Statements => New_List (
- Make_If_Statement (Data.Loc,
- Condition =>
- Make_Op_Not (Data.Loc,
- Right_Opnd => New_Reference_To (Data.Raised_Id, Data.Loc)),
-
- Then_Statements => New_List (
- Make_Assignment_Statement (Data.Loc,
- Name => New_Reference_To (Data.Raised_Id, Data.Loc),
- Expression => New_Reference_To (Standard_True, Data.Loc)),
-
- Make_Procedure_Call_Statement (Data.Loc,
- Name =>
- New_Reference_To (Proc_To_Call, Data.Loc),
- Parameter_Associations => Actuals)))));
+ Exception_Choices => New_List (Make_Others_Choice (Data.Loc)),
+ Statements => Stmts);
end Build_Exception_Handler;
-------------------------------
return;
end if;
- Data.Abort_Id := Make_Temporary (Loc, 'A');
- Data.E_Id := Make_Temporary (Loc, 'E');
Data.Raised_Id := Make_Temporary (Loc, 'R');
-- In certain scenarios, finalization can be triggered by an abort. If
and then VM_Target = No_VM
and then not For_Package
then
+ Data.Abort_Id := Make_Temporary (Loc, 'A');
+
A_Expr := New_Reference_To (RTE (RE_Triggered_By_Abort), Loc);
- -- No abort, .NET/JVM or library-level finalizers
+ -- Generate:
+ -- Abort_Id : constant Boolean := <A_Expr>;
+
+ Append_To (Decls,
+ Make_Object_Declaration (Loc,
+ Defining_Identifier => Data.Abort_Id,
+ Constant_Present => True,
+ Object_Definition => New_Reference_To (Standard_Boolean, Loc),
+ Expression => A_Expr));
else
- A_Expr := New_Reference_To (Standard_False, Loc);
+ -- No abort, .NET/JVM or library-level finalizers
+
+ Data.Abort_Id := Empty;
end if;
- -- Generate:
- -- Abort_Id : constant Boolean := <A_Expr>;
+ if Exception_Extra_Info then
+ Data.E_Id := Make_Temporary (Loc, 'E');
- Append_To (Decls,
- Make_Object_Declaration (Loc,
- Defining_Identifier => Data.Abort_Id,
- Constant_Present => True,
- Object_Definition => New_Reference_To (Standard_Boolean, Loc),
- Expression => A_Expr));
+ -- Generate:
+ -- E_Id : Exception_Occurrence;
- -- Generate:
- -- E_Id : Exception_Occurrence;
+ E_Decl :=
+ Make_Object_Declaration (Loc,
+ Defining_Identifier => Data.E_Id,
+ Object_Definition =>
+ New_Reference_To (RTE (RE_Exception_Occurrence), Loc));
+ Set_No_Initialization (E_Decl);
- E_Decl :=
- Make_Object_Declaration (Loc,
- Defining_Identifier => Data.E_Id,
- Object_Definition =>
- New_Reference_To (RTE (RE_Exception_Occurrence), Loc));
- Set_No_Initialization (E_Decl);
+ Append_To (Decls, E_Decl);
- Append_To (Decls, E_Decl);
+ else
+ Data.E_Id := Empty;
+ end if;
-- Generate:
-- Raised_Id : Boolean := False;
(Data : Finalization_Exception_Data) return Node_Id
is
Stmt : Node_Id;
+ Expr : Node_Id;
begin
-- Standard run-time and .NET/JVM targets use the specialized routine
-- Raise_From_Controlled_Operation.
- if RTE_Available (RE_Raise_From_Controlled_Operation) then
+ if Exception_Extra_Info
+ and then RTE_Available (RE_Raise_From_Controlled_Operation)
+ then
Stmt :=
Make_Procedure_Call_Statement (Data.Loc,
Name =>
Reason => PE_Finalize_Raised_Exception);
end if;
+ -- Generate:
+ -- Raised_Id and then not Abort_Id
+ -- <or>
+ -- Raised_Id
+
+ Expr := New_Reference_To (Data.Raised_Id, Data.Loc);
+
+ if Present (Data.Abort_Id) then
+ Expr := Make_And_Then (Data.Loc,
+ Left_Opnd => Expr,
+ Right_Opnd =>
+ Make_Op_Not (Data.Loc,
+ Right_Opnd => New_Reference_To (Data.Abort_Id, Data.Loc)));
+ end if;
+
-- Generate:
-- if Raised_Id and then not Abort_Id then
-- Raise_From_Controlled_Operation (E_Id);
return
Make_If_Statement (Data.Loc,
- Condition =>
- Make_And_Then (Data.Loc,
- Left_Opnd => New_Reference_To (Data.Raised_Id, Data.Loc),
- Right_Opnd =>
- Make_Op_Not (Data.Loc,
- Right_Opnd => New_Reference_To (Data.Abort_Id, Data.Loc))),
-
+ Condition => Expr,
Then_Statements => New_List (Stmt));
end Build_Raise_Statement;
projects / gcc.git / commitdiff