aboutsummaryrefslogtreecommitdiff
path: root/gcc/ada/ghost.ads
diff options
context:
space:
mode:
authorHristian Kirtchev <kirtchev@adacore.com>2018-07-17 08:06:24 +0000
committerPierre-Marie de Rodat <pmderodat@gcc.gnu.org>2018-07-17 08:06:24 +0000
commit980f94b75b8ccd47afa55c6109a5899f325a61ee (patch)
tree536002f95a4bbf2667c82ef74652e1dc6d85712b /gcc/ada/ghost.ads
parente8427749a9c5ad6ec2c0653dcc4edea5b41efc31 (diff)
downloadgcc-980f94b75b8ccd47afa55c6109a5899f325a61ee.zip
gcc-980f94b75b8ccd47afa55c6109a5899f325a61ee.tar.gz
gcc-980f94b75b8ccd47afa55c6109a5899f325a61ee.tar.bz2
[Ada] New ignored Ghost code removal mechanism
This patch reimplements the mechanism which removes ignored Ghost code from the tree. The previous mechanism proved to be unreliable because it assumed that no new scoping constructs would be created after some ignored Ghost code had already notified its enclosing scoping constructs that they contain such code. The assumption can be broken by having a call to an ignored Ghost procedure within the extended return statement of a function. The procedure call would signal the enclosing function that it contains ignored Ghost code, however the return statement would introduce an extra block, effectively hiding the procedure call from the ignored Ghost code elimination pass. The new mechanism implemented in this patch forgoes directed tree pruning in favor of storing the actual ignored Ghost code, and later directly eliminating it from the tree. For this approach to operate efficiently, only "top level" ignored Ghost constructs are stored. The top level constructs are essentially nodes which can appear within a declarative or statement list and be safely rewritten into null statements. This ensures that only "root" ignored Ghost construct need to be processed, as opposed to all ignored Ghost nodes within a subtree. The approach has one drawback however. Due to the generation and analysis of ignored Ghost code, a construct may be recorded multiple times (usually twice). The mechanism simply deals with this artefact instead of employing expensive solutions such as hash tables or a common flag shared by all nodes to eliminate the duplicates. ------------ -- Source -- ------------ -- main.adb with Ada.Text_IO; use Ada.Text_IO; procedure Main is procedure Ghost_Proc with Ghost; procedure Ghost_Proc is begin Put_Line ("ERROR: Ghost_Proc called"); end Ghost_Proc; function Func return Integer is begin return Res : Integer := 123 do Ghost_Proc; end return; end Func; Val : Integer with Ghost; begin Val := Func; end Main; ---------------------------- -- Compilation and output -- ---------------------------- $ gcc -c -gnatDG main.adb $ grep -c "ghost" main.adb.dg 0 2018-07-17 Hristian Kirtchev <kirtchev@adacore.com> gcc/ada/ * alloc.ads: Update the allocation metrics of the ignored Ghost nodes table. * atree.adb: Add a soft link for a procedure which is invoked whenever an ignored Ghost node or entity is created. (Change_Node): Preserve relevant attributes which come from the Flags table. (Mark_New_Ghost_Node): Record a newly created ignored Ghost node or entity. (Rewrite): Preserve relevant attributes which come from the Flags table. (Set_Ignored_Ghost_Recording_Proc): New routine. * atree.ads: Define an access-to-suprogram type for a soft link which records a newly created ignored Ghost node or entity. (Set_Ignored_Ghost_Recording_Proc): New routine. * ghost.adb: Remove with and use clause for Lib. Remove table Ignored_Ghost_Units. Add new table Ignored_Ghost_Nodes. (Add_Ignored_Ghost_Unit): Removed. (Initialize): Initialize the table which stores ignored Ghost nodes. Set the soft link which allows Atree.Mark_New_Ghost_Node to record an ignored Ghost node. (Is_Ignored_Ghost_Unit): Use the ultimate original node when checking an eliminated ignored Ghost unit. (Lock): Release and lock the table which stores ignored Ghost nodes. (Mark_And_Set_Ghost_Assignment): Record rather than propagate ignored Ghost nodes. (Mark_And_Set_Ghost_Procedure_Call): Record rather than propagate ignored Ghost nodes. (Mark_Ghost_Clause): Record rather than propagate ignored Ghost nodes. (Mark_Ghost_Declaration_Or_Body): Record rather than propagate ignored Ghost nodes. (Mark_Ghost_Pragma): Record rather than propagate ignored Ghost nodes. (Propagate_Ignored_Ghost_Code): Removed. (Record_Ignored_Ghost_Node): New routine. (Remove_Ignored_Ghost_Code): Reimplemented. (Remove_Ignored_Ghost_Node): New routine. (Ultimate_Original_Node): New routine. * ghost.ads (Check_Ghost_Completion): Removed. * sem_ch8.adb (Analyze_Use_Package): Remove obsolete code. Mark a use package clause as ignored Ghost if applicable. * sem_util.adb (Is_Body_Or_Package_Declaration): Reimplemented. From-SVN: r262775
Diffstat (limited to 'gcc/ada/ghost.ads')
-rw-r--r--gcc/ada/ghost.ads4
1 files changed, 0 insertions, 4 deletions
diff --git a/gcc/ada/ghost.ads b/gcc/ada/ghost.ads
index ef95116..c079595 100644
--- a/gcc/ada/ghost.ads
+++ b/gcc/ada/ghost.ads
@@ -31,10 +31,6 @@ with Types; use Types;
package Ghost is
- procedure Add_Ignored_Ghost_Unit (Unit : Node_Id);
- -- Add a single ignored Ghost compilation unit to the internal table for
- -- post processing.
-
procedure Check_Ghost_Completion
(Prev_Id : Entity_Id;
Compl_Id : Entity_Id);