r262775 - in /trunk/gcc/ada: ChangeLog alloc.ad...

[pmderodat at gcc dot gnu dot org]

Author: pmderodat
Date: Tue Jul 17 08:06:24 2018
New Revision: 262775

URL: https://gcc.gnu.org/viewcvs?rev=262775&root=gcc&view=rev
Log:
[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.

Modified:
    trunk/gcc/ada/ChangeLog
    trunk/gcc/ada/alloc.ads
    trunk/gcc/ada/atree.adb
    trunk/gcc/ada/atree.ads
    trunk/gcc/ada/ghost.adb
    trunk/gcc/ada/ghost.ads
    trunk/gcc/ada/sem_ch8.adb
    trunk/gcc/ada/sem_util.adb