File : scos.ads


   1 ------------------------------------------------------------------------------
   2 --                                                                          --
   3 --                         GNAT COMPILER COMPONENTS                         --
   4 --                                                                          --
   5 --                                 S C O S                                  --
   6 --                                                                          --
   7 --                                 S p e c                                  --
   8 --                                                                          --
   9 --          Copyright (C) 2009-2015, Free Software Foundation, Inc.         --
  10 --                                                                          --
  11 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
  12 -- terms of the  GNU General Public License as published  by the Free Soft- --
  13 -- ware  Foundation;  either version 3,  or (at your option) any later ver- --
  14 -- sion.  GNAT is distributed in the hope that it will be useful, but WITH- --
  15 -- OUT ANY WARRANTY;  without even the  implied warranty of MERCHANTABILITY --
  16 -- or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License --
  17 -- for  more details.  You should have  received  a copy of the GNU General --
  18 -- Public License  distributed with GNAT; see file COPYING3.  If not, go to --
  19 -- http://www.gnu.org/licenses for a complete copy of the license.          --
  20 --                                                                          --
  21 -- GNAT was originally developed  by the GNAT team at  New York University. --
  22 -- Extensive contributions were provided by Ada Core Technologies Inc.      --
  23 --                                                                          --
  24 ------------------------------------------------------------------------------
  25 
  26 --  This package defines tables used to store Source Coverage Obligations. It
  27 --  is used by Par_SCO to build the SCO information before writing it out to
  28 --  the ALI file, and by Get_SCO/Put_SCO to read and write the text form that
  29 --  is used in the ALI file.
  30 
  31 with Namet; use Namet;
  32 with Types; use Types;
  33 
  34 with GNAT.Table;
  35 
  36 package SCOs is
  37 
  38    --  SCO information can exist in one of two forms. In the ALI file, it is
  39    --  represented using a text format that is described in this specification.
  40    --  Internally it is stored using two tables SCO_Table and SCO_Unit_Table,
  41    --  which are also defined in this unit.
  42 
  43    --  Par_SCO is part of the compiler. It scans the parsed source tree and
  44    --  populates the internal tables.
  45 
  46    --  Get_SCO reads the text lines in ALI format and populates the internal
  47    --  tables with corresponding information.
  48 
  49    --  Put_SCO reads the internal tables and generates text lines in the ALI
  50    --  format.
  51 
  52    --  WARNING: There are C bindings for this package. Any changes to this
  53    --  source file must be properly reflected in the C header file scos.h
  54 
  55    --------------------
  56    -- SCO ALI Format --
  57    --------------------
  58 
  59    --  Source coverage obligations are generated on a unit-by-unit basis in the
  60    --  ALI file, using lines that start with the identifying character C. These
  61    --  lines are generated if the -gnateS switch is set.
  62 
  63    --  Sloc Ranges
  64 
  65    --    In several places in the SCO lines, Sloc ranges appear. These are used
  66    --    to indicate the first and last Sloc of some construct in the tree and
  67    --    they have the form:
  68 
  69    --      line:col-line:col
  70 
  71    --    Note that SCO's are generated only for generic templates, not for
  72    --    generic instances (since only the first are part of the source). So
  73    --    we don't need generic instantiation stuff in these line:col items.
  74 
  75    --  SCO File headers
  76 
  77    --    The SCO information follows the cross-reference information, so it
  78    --    need not be read by tools like gnatbind, gnatmake etc. The SCO output
  79    --    is divided into sections, one section for each unit for which SCO's
  80    --    are generated. A SCO section has a header of the form:
  81 
  82    --      C dependency-number filename
  83 
  84    --        This header precedes SCO information for the unit identified by
  85    --        dependency number and file name. The dependency number is the
  86    --        index into the generated D lines and is ones origin (i.e. 2 =
  87    --        reference to second generated D line).
  88 
  89    --        Note that the filename here will reflect the original name if
  90    --        a Source_Reference pragma was encountered (since all line number
  91    --        references will be with respect to the original file).
  92 
  93    --        Note: the filename is redundant in that it could be deduced from
  94    --        the corresponding D line, but it is convenient at least for human
  95    --        reading of the SCO information, and means that the SCO information
  96    --        can stand on its own without needing other parts of the ALI file.
  97 
  98    --  Statements
  99 
 100    --    For the purpose of SCO generation, the notion of statement includes
 101    --    simple statements and also the following declaration types:
 102 
 103    --      type_declaration
 104    --      subtype_declaration
 105    --      object_declaration
 106    --      renaming_declaration
 107    --      generic_instantiation
 108 
 109    --    and the following regions of the syntax tree:
 110 
 111    --      the part of a case_statement from CASE up to the expression
 112    --      the part of a FOR loop iteration scheme from FOR up to the
 113    --        loop_parameter_specification
 114    --      the part of a WHILE loop up to the condition
 115    --      the part of an extended_return_statement from RETURN up to the
 116    --        expression (if present) or to the return_subtype_indication (if
 117    --        no expression)
 118 
 119    --    and any pragma that occurs at a place where a statement or declaration
 120    --    is allowed.
 121 
 122    --  Statement lines
 123 
 124    --    These lines correspond to one or more successive statements (in the
 125    --    sense of the above list) which are always executed in sequence (in the
 126    --    absence of exceptions or other external interruptions).
 127 
 128    --    Entry points to such sequences are:
 129 
 130    --      the first declaration of any declarative_part
 131    --      the first statement of any sequence_of_statements that is not in a
 132    --        body or block statement that has a non-empty declarative part
 133    --      the first statement after a compound statement
 134    --      the first statement after an EXIT, RAISE or GOTO statement
 135    --      any statement with a label (the label itself is not part of the
 136    --       entry point that is recorded).
 137 
 138    --    Each entry point must appear as the first statement entry on a CS
 139    --    line. Thus, if any simple statement on a CS line is known to have
 140    --    been executed, then all statements that appear before it on the same
 141    --    CS line are certain to also have been executed.
 142 
 143    --    The form of a statement line in the ALI file is:
 144 
 145    --      CS [dominance] *sloc-range [*sloc-range...]
 146 
 147    --    where each sloc-range corresponds to a single statement, and * is
 148    --    one of:
 149 
 150    --      t        type declaration
 151    --      s        subtype declaration
 152    --      o        object declaration
 153    --      r        renaming declaration
 154    --      i        generic instantiation
 155    --      A        ACCEPT statement (from ACCEPT to end of parameter profile)
 156    --      C        CASE statement (from CASE to end of expression)
 157    --      E        EXIT statement
 158    --      F        FOR loop (from FOR to end of iteration scheme)
 159    --      I        IF statement (from IF to end of condition)
 160    --      P[name:] PRAGMA with the indicated name
 161    --      p[name:] disabled PRAGMA with the indicated name
 162    --      R        extended RETURN statement
 163    --      S        SELECT statement
 164    --      W        WHILE loop statement (from WHILE to end of condition)
 165 
 166    --      Note: for I and W, condition above is in the RM syntax sense (this
 167    --      condition is a decision in SCO terminology).
 168 
 169    --    and is omitted for all other cases
 170 
 171    --    The optional dominance marker is of the form gives additional
 172    --    information as to how the sequence of statements denoted by the CS
 173    --    line can be entered:
 174 
 175    --      >F<sloc>
 176    --        sequence is entered only if the decision at <sloc> is False
 177    --      >T<sloc>
 178    --        sequence is entered only if the decision at <sloc> is True
 179 
 180    --      >S<sloc>
 181    --        sequence is entered only if the statement at <sloc> has been
 182    --        executed
 183 
 184    --      >E<sloc-range>
 185    --        sequence is the sequence of statements for a exception_handler
 186    --        with the given sloc range
 187 
 188    --    Note: up to 6 entries can appear on a single CS line. If more than 6
 189    --    entries appear in one logical statement sequence, continuation lines
 190    --    are marked by Cs and appear immediately after the CS line.
 191 
 192    --    Implementation permission: a SCO generator is permitted to emit a
 193    --    narrower SLOC range for a statement if the corresponding code
 194    --    generation circuitry ensures that all debug information for the code
 195    --    implementing the statement will be labeled with SLOCs that fall within
 196    --    that narrower range.
 197 
 198    --  Decisions
 199 
 200    --    Note: in the following description, logical operator includes only the
 201    --    short-circuited forms and NOT (so can be only NOT, AND THEN, OR ELSE).
 202    --    The reason that we can exclude AND/OR/XOR is that we expect SCO's to
 203    --    be generated using the restriction No_Direct_Boolean_Operators if we
 204    --    are interested in decision coverage, which does not permit the use of
 205    --    AND/OR/XOR on boolean operands. These are permitted on modular integer
 206    --    types, but such operations do not count as decisions in any case. If
 207    --    we are generating SCO's only for simple coverage, then we are not
 208    --    interested in decisions in any case.
 209 
 210    --    Note: the reason we include NOT is for informational purposes. The
 211    --    presence of NOT does not generate additional coverage obligations,
 212    --    but if we know where the NOT's are, the coverage tool can generate
 213    --    more accurate diagnostics on uncovered tests.
 214 
 215    --    A top level boolean expression is a boolean expression that is not an
 216    --    operand of a logical operator.
 217 
 218    --    Decisions are either simple or complex. A simple decision is a top
 219    --    level boolean expression that has only one condition and that occurs
 220    --    in the context of a control structure in the source program, including
 221    --    WHILE, IF, EXIT WHEN, or immediately within an Assert, Check,
 222    --    Pre_Condition or Post_Condition pragma, or as the first argument of a
 223    --    dyadic pragma Debug. Note that a top level boolean expression with
 224    --    only one condition that occurs in any other context, for example as
 225    --    right hand side of an assignment, is not considered to be a (simple)
 226    --    decision.
 227 
 228    --    A complex decision is a top level boolean expression that has more
 229    --    than one condition. A complex decision may occur in any boolean
 230    --    expression context.
 231 
 232    --    So for example, if we have
 233 
 234    --        A, B, C, D : Boolean;
 235    --        function F (Arg : Boolean) return Boolean);
 236    --        ...
 237    --        A and then (B or else F (C and then D))
 238 
 239    --    There are two (complex) decisions here:
 240 
 241    --        1. X and then (Y or else Z)
 242 
 243    --           where X = A, Y = B, and Z = F (C and then D)
 244 
 245    --        2. C and then D
 246 
 247    --    For each decision, a decision line is generated with the form:
 248 
 249    --      C* sloc expression
 250 
 251    --    Here * is one of the following:
 252 
 253    --      E       decision in EXIT WHEN statement
 254    --      G       decision in entry guard
 255    --      I       decision in IF statement or if expression
 256    --      P       decision in pragma Assert / Check / Pre/Post_Condition
 257    --      A[name] decision in aspect Pre/Post (aspect name optional)
 258    --      W       decision in WHILE iteration scheme
 259    --      X       decision in some other expression context
 260 
 261    --    For E, G, I, P, W, sloc is the source location of the EXIT, ENTRY, IF,
 262    --    PRAGMA or WHILE token, respectively
 263 
 264    --    For A sloc is the source location of the aspect identifier
 265 
 266    --    For X, sloc is omitted
 267 
 268    --    The expression is a prefix polish form indicating the structure of
 269    --    the decision, including logical operators and short-circuit forms.
 270    --    The following is a grammar showing the structure of expression:
 271 
 272    --      expression ::= term             (if expr is not logical operator)
 273    --      expression ::= &sloc term term  (if expr is AND or AND THEN)
 274    --      expression ::= |sloc term term  (if expr is OR or OR ELSE)
 275    --      expression ::= !sloc term       (if expr is NOT)
 276 
 277    --      In the last three cases, sloc is the source location of the AND, OR,
 278    --      or NOT token, respectively.
 279 
 280    --      term ::= element
 281    --      term ::= expression
 282 
 283    --      element ::= *sloc-range
 284 
 285    --    where * is one of the following letters:
 286 
 287    --      c  condition
 288    --      t  true condition
 289    --      f  false condition
 290 
 291    --      t/f are used to mark a condition that has been recognized by the
 292    --      compiler as always being true or false. c is the normal case of
 293    --      conditions whose value is not known at compile time.
 294 
 295    --    & indicates AND THEN connecting two conditions
 296 
 297    --    | indicates OR ELSE connecting two conditions
 298 
 299    --    ! indicates NOT applied to the expression
 300 
 301    --    Note that complex decisions do NOT include non-short-circuited logical
 302    --    operators (AND/XOR/OR). In the context of existing coverage tools the
 303    --    No_Direct_Boolean_Operators restriction is assumed, so these operators
 304    --    cannot appear in the source in any case.
 305 
 306    --    The SCO line for a decision always occurs after the CS line for the
 307    --    enclosing statement. The SCO line for a nested decision always occurs
 308    --    after the line for the enclosing decision.
 309 
 310    --    Note that membership tests are considered to be a single simple
 311    --    condition, and that is true even if the Ada 2005 set membership
 312    --    form is used, e.g. A in (2,7,11.15).
 313 
 314    --    Implementation permission: a SCO generator is permitted to emit a
 315    --    narrower SLOC range for a condition if the corresponding code
 316    --    generation circuitry ensures that all debug information for the code
 317    --    evaluating the condition will be labeled with SLOCs that fall within
 318    --    that narrower range.
 319 
 320    --  Case Expressions
 321 
 322    --    For case statements, we rely on statement coverage to make sure that
 323    --    all branches of a case statement are covered, but that does not work
 324    --    for case expressions, since the entire expression is contained in a
 325    --    single statement. However, for complete coverage we really should be
 326    --    able to check that every branch of the case statement is covered, so
 327    --    we generate a SCO of the form:
 328 
 329    --      CC sloc-range sloc-range ...
 330 
 331    --    where sloc-range covers the range of the case expression
 332 
 333    --    Note: up to 6 entries can appear on a single CC line. If more than 6
 334    --    entries appear in one logical statement sequence, continuation lines
 335    --    are marked by Cc and appear immediately after the CC line.
 336 
 337    --  Generic instances
 338 
 339    --    A table of all generic instantiations in the compilation is generated
 340    --    whose entries have the form:
 341 
 342    --      C i index dependency-number|sloc [enclosing]
 343 
 344    --    Where index is the 1-based index of the entry in the table,
 345    --    dependency-number and sloc indicate the source location of the
 346    --    instantiation, and enclosing is the index of the enclosing
 347    --    instantiation in the table (for a nested instantiation), or is
 348    --    omitted for an outer instantiation.
 349 
 350    --  Disabled pragmas
 351 
 352    --    No SCO is generated for disabled pragmas
 353 
 354    ---------------------------------------------------------------------
 355    -- Internal table used to store Source Coverage Obligations (SCOs) --
 356    ---------------------------------------------------------------------
 357 
 358    type Source_Location is record
 359       Line : Logical_Line_Number;
 360       Col  : Column_Number;
 361    end record;
 362 
 363    No_Source_Location : constant Source_Location :=
 364                           (No_Line_Number, No_Column_Number);
 365 
 366    type SCO_Table_Entry is record
 367       From : Source_Location := No_Source_Location;
 368       To   : Source_Location := No_Source_Location;
 369       C1   : Character       := ' ';
 370       C2   : Character       := ' ';
 371       Last : Boolean         := False;
 372 
 373       Pragma_Sloc : Source_Ptr := No_Location;
 374       --  For the decision SCO of a pragma, or for the decision SCO of any
 375       --  expression nested in a pragma Debug/Assert/PPC, location of PRAGMA
 376       --  token (used for control of SCO output, value not recorded in ALI
 377       --  file). Similarly, for the decision SCO of an aspect, or for the
 378       --  decision SCO of any expression nested in an aspect, location of
 379       --  aspect identifier token.
 380 
 381       Pragma_Aspect_Name : Name_Id := No_Name;
 382       --  For the SCO for a pragma/aspect, gives the pragma/apsect name
 383    end record;
 384 
 385    package SCO_Table is new GNAT.Table (
 386      Table_Component_Type => SCO_Table_Entry,
 387      Table_Index_Type     => Nat,
 388      Table_Low_Bound      => 1,
 389      Table_Initial        => 500,
 390      Table_Increment      => 300);
 391 
 392    Is_Decision : constant array (Character) of Boolean :=
 393      ('E' | 'G' | 'I' | 'P' | 'a' | 'A' | 'W' | 'X' => True,
 394       others                                        => False);
 395    --  Indicates which C1 values correspond to decisions
 396 
 397    --  The SCO_Table_Entry values appear as follows:
 398 
 399    --    Statements
 400    --      C1   = 'S'
 401    --      C2   = statement type code to appear on CS line (or ' ' if none)
 402    --      From = starting source location
 403    --      To   = ending source location
 404    --      Last = False for all but the last entry, True for last entry
 405 
 406    --    Note: successive statements (possibly interspersed with entries of
 407    --    other kinds, that are ignored for this purpose), starting with one
 408    --    labeled with C1 = 'S', up to and including the first one labeled with
 409    --    Last = True, indicate the sequence to be output for a sequence of
 410    --    statements on a single CS line (possibly followed by Cs continuation
 411    --    lines).
 412 
 413    --    Note: for a pragma that may be disabled (Debug, Assert, PPC, Check),
 414    --    the entry is initially created with C2 = 'p', to mark it as disabled.
 415    --    Later on during semantic analysis, if the pragma is enabled,
 416    --    Set_SCO_Pragma_Enabled changes C2 to 'P' to cause the entry to be
 417    --    emitted in Put_SCOs.
 418 
 419    --    Dominance marker
 420    --      C1   = '>'
 421    --      C2   = 'F'/'T'/'S'/'E'
 422    --      From = Decision/statement sloc ('F'/'T'/'S'),
 423    --             handler first sloc ('E')
 424    --      To   = No_Source_Location ('F'/'T'/'S'), handler last sloc ('E')
 425 
 426    --    Note: A dominance marker is always followed by a statement entry
 427 
 428    --    Decision (EXIT/entry guard/IF/WHILE)
 429    --      C1   = 'E'/'G'/'I'/'W' (for EXIT/entry Guard/IF/WHILE)
 430    --      C2   = ' '
 431    --      From = EXIT/ENTRY/IF/WHILE token
 432    --      To   = No_Source_Location
 433    --      Last = unused
 434 
 435    --    Decision (PRAGMA)
 436    --      C1   = 'P'
 437    --      C2   = ' '
 438    --      From = PRAGMA token
 439    --      To   = No_Source_Location
 440    --      Last = unused
 441 
 442    --    Note: when the parse tree is first scanned, we unconditionally build a
 443    --    pragma decision entry for any decision in a pragma (here as always in
 444    --    SCO contexts, the only pragmas with decisions are Assert, Check,
 445    --    dyadic Debug, Precondition and Postcondition). These entries will
 446    --    be omitted in output if the pragma is disabled (see comments for
 447    --    statement entries): this filtering is achieved during the second pass
 448    --    of SCO generation (Par_SCO.SCO_Record_Filtered).
 449 
 450    --    Decision (ASPECT)
 451    --      C1   = 'A'
 452    --      C2   = ' '
 453    --      From = aspect identifier
 454    --      To   = No_Source_Location
 455    --      Last = unused
 456 
 457    --    Note: when the parse tree is first scanned, we unconditionally build a
 458    --    pragma decision entry for any decision in an aspect (Pre/Post/
 459    --    [Type_]Invariant/[Static_|Dynamic_]Predicate). Entries for disabled
 460    --    Pre/Post aspects will be omitted from output.
 461 
 462    --    Decision (Expression)
 463    --      C1   = 'X'
 464    --      C2   = ' '
 465    --      From = No_Source_Location
 466    --      To   = No_Source_Location
 467    --      Last = unused
 468 
 469    --    Operator
 470    --      C1   = '!', '&', '|'
 471    --      C2   = ' '/'?'/ (Logical operator/Putative one)
 472    --      From = location of NOT/AND/OR token
 473    --      To   = No_Source_Location
 474    --      Last = False
 475 
 476    --    Element (condition)
 477    --      C1   = ' '
 478    --      C2   = 'c', 't', or 'f' (condition/true/false)
 479    --      From = starting source location
 480    --      To   = ending source location
 481    --      Last = False for all but the last entry, True for last entry
 482 
 483    --    Note: the sequence starting with a decision, and continuing with
 484    --    operators and elements up to and including the first one labeled with
 485    --    Last = True, indicate the sequence to be output on one decision line.
 486 
 487    ----------------
 488    -- Unit Table --
 489    ----------------
 490 
 491    --  This table keeps track of the units and the corresponding starting and
 492    --  ending indexes (From, To) in the SCO table. Note that entry zero is
 493    --  present but unused, it is for convenience in calling the sort routine.
 494    --  Thus the lower bound for real entries is 1.
 495 
 496    type SCO_Unit_Index is new Int;
 497    --  Used to index values in this table. Values start at 1 and are assigned
 498    --  sequentially as entries are constructed.
 499 
 500    type SCO_Unit_Table_Entry is record
 501       File_Name : String_Ptr;
 502       --  Pointer to file name in ALI file
 503 
 504       File_Index : Source_File_Index;
 505       --  Index for the source file
 506 
 507       Dep_Num : Nat;
 508       --  Dependency number in ALI file
 509 
 510       From : Nat;
 511       --  Starting index in SCO_Table of SCO information for this unit
 512 
 513       To : Nat;
 514       --  Ending index in SCO_Table of SCO information for this unit
 515 
 516       --  Warning: SCOs generation (in Par_SCO) is done in two passes, which
 517       --  communicate through an intermediate table (Par_SCO.SCO_Raw_Table).
 518       --  Before the second pass executes, From and To actually reference index
 519       --  in the internal table: SCO_Table is empty. Then, at the end of the
 520       --  second pass, these indexes are updated in order to reference indexes
 521       --  in SCO_Table.
 522 
 523    end record;
 524 
 525    package SCO_Unit_Table is new GNAT.Table (
 526      Table_Component_Type => SCO_Unit_Table_Entry,
 527      Table_Index_Type     => SCO_Unit_Index,
 528      Table_Low_Bound      => 0, -- see note above on sorting
 529      Table_Initial        => 20,
 530      Table_Increment      => 200);
 531 
 532    -----------------------
 533    -- Generic instances --
 534    -----------------------
 535 
 536    type SCO_Instance_Index is new Nat;
 537 
 538    type SCO_Instance_Table_Entry is record
 539       Inst_Dep_Num : Nat;
 540       Inst_Loc     : Source_Location;
 541       --  File and source location of instantiation
 542 
 543       Enclosing_Instance : SCO_Instance_Index;
 544    end record;
 545 
 546    package SCO_Instance_Table is new GNAT.Table (
 547      Table_Component_Type => SCO_Instance_Table_Entry,
 548      Table_Index_Type     => SCO_Instance_Index,
 549      Table_Low_Bound      => 1,
 550      Table_Initial        => 20,
 551      Table_Increment      => 200);
 552 
 553    -----------------
 554    -- Subprograms --
 555    -----------------
 556 
 557    procedure Initialize;
 558    --  Reset tables for a new compilation
 559 
 560 end SCOs;