Skip to content

Commit b458dab

Browse files
committed
SC_Obligations: assert SCOs nesting/ordering invariants for scopes
The scope entities traversal code assumes that SCOs ranges in scope entities (Scope_Entity.From/.To) are correctly nested/ordered in scope entities trees. Add code to check that this invariant is respected each time we create/modify these trees. These invariants are supposed to hold no matter how gnatcov is used and checking them is not trivial, so check them only when assertions are enabled.
1 parent 017c1a4 commit b458dab

File tree

1 file changed

+120
-0
lines changed

1 file changed

+120
-0
lines changed

tools/gnatcov/sc_obligations.adb

Lines changed: 120 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,7 @@
1919
-- Source Coverage Obligations
2020

2121
with Ada.Characters.Handling; use Ada.Characters.Handling;
22+
with Ada.Exceptions;
2223
with Ada.Strings.Fixed; use Ada.Strings.Fixed;
2324
with Ada.Streams; use Ada.Streams;
2425
with Ada.Text_IO; use Ada.Text_IO;
@@ -50,6 +51,17 @@ package body SC_Obligations is
5051
No_Location : Source_Location renames Slocs.No_Location;
5152
-- (not SCOs.Source_Location)
5253

54+
function SCOs_Nested_And_Ordered
55+
(Tree : Scope_Entities_Trees.Tree) return Boolean;
56+
-- Return whether nodes in Tree are:
57+
--
58+
-- * properly nested: SCO ranges (Element.From .. Element.To) are disjoint
59+
-- for two sibling elements, and all nodes' SCO ranges are included in
60+
-- its parents';
61+
--
62+
-- * properly ordered: if E1 and E2 are consecutive siblings, E1.To must be
63+
-- smaller than E2.From.
64+
5365
---------------
5466
-- Instances --
5567
---------------
@@ -1242,6 +1254,7 @@ package body SC_Obligations is
12421254

12431255
Available_Subps_Of_Interest.Include (Scope_Ent.Identifier);
12441256
end loop;
1257+
pragma Assert (SCOs_Nested_And_Ordered (CP_CU.Scope_Entities));
12451258

12461259
end if;
12471260

@@ -4362,6 +4375,106 @@ package body SC_Obligations is
43624375
return Scope_Entities_Trees.Empty_Tree;
43634376
end Get_Scope_Entities;
43644377

4378+
-----------------------------
4379+
-- SCOs_Nested_And_Ordered --
4380+
-----------------------------
4381+
4382+
function SCOs_Nested_And_Ordered
4383+
(Tree : Scope_Entities_Trees.Tree) return Boolean
4384+
is
4385+
use Scope_Entities_Trees;
4386+
4387+
Failure : exception;
4388+
-- Exception raised when the nesting/ordering invariant is found to be
4389+
-- broken.
4390+
4391+
Lower_Bound : SCO_Id := No_SCO_Id;
4392+
-- At every step of the check, this designates the minimum possible SCO
4393+
-- value for the .From component for the next element to inspect.
4394+
4395+
procedure Check_Element (Cur : Cursor);
4396+
-- Check that Cur's From/To SCOs range is not empty and
4397+
-- Parent_From .. Parent_To range and that they are correctly ordered.
4398+
4399+
-------------------
4400+
-- Check_Element --
4401+
-------------------
4402+
4403+
procedure Check_Element (Cur : Cursor) is
4404+
SE : Scope_Entity renames Tree.Constant_Reference (Cur);
4405+
Child : Cursor := First_Child (Cur);
4406+
4407+
Last : SCO_Id;
4408+
-- SCO range upper bound for Cur's last child, or SE.From if there is
4409+
-- no child.
4410+
begin
4411+
-- Check that SCO ranges are never empty
4412+
4413+
if SE.From > SE.To then
4414+
raise Failure with "empty SCO range for " & Image (SE);
4415+
end if;
4416+
4417+
-- Check that the SCO range lower bound is both:
4418+
--
4419+
-- * greater or equal to the parent's lower bound (this is the first
4420+
-- half of the nesting check;
4421+
--
4422+
-- * greater than the previous sibling (if any: this checks the
4423+
-- ordering).
4424+
4425+
if SE.From < Lower_Bound then
4426+
raise Failure with "SCO lower bound too low for " & Image (SE);
4427+
end if;
4428+
Lower_Bound := SE.From;
4429+
Last := SE.From;
4430+
4431+
while Has_Element (Child) loop
4432+
Check_Element (Child);
4433+
Child := Next_Sibling (Child);
4434+
Last := Lower_Bound;
4435+
4436+
-- The next sibling's SCO range cannot overlap with the current's
4437+
4438+
Lower_Bound := Lower_Bound + 1;
4439+
end loop;
4440+
4441+
-- Check that the SCO range upper bound is greater or equal to
4442+
-- the upper bound of the last child's upper bound (this is the
4443+
-- second half of the nesting check).
4444+
4445+
if SE.To < Last then
4446+
raise Failure with "SCO higher bound too low for " & Image (SE);
4447+
end if;
4448+
Lower_Bound := SE.To;
4449+
end Check_Element;
4450+
4451+
Cur : Cursor := First_Child (Tree.Root);
4452+
4453+
-- Start of processing for SCOs_Nested_And_Ordered
4454+
4455+
begin
4456+
while Has_Element (Cur) loop
4457+
Check_Element (Cur);
4458+
Cur := Next_Sibling (Cur);
4459+
end loop;
4460+
return True;
4461+
4462+
exception
4463+
when Exc : Failure =>
4464+
4465+
-- In case of failure, be helpful and print the offending tree for
4466+
-- the verbose mode.
4467+
4468+
if Verbose then
4469+
Put_Line
4470+
("The following tree of scopes breaks the nesting/ordering"
4471+
& " invariant:");
4472+
Put_Line (Ada.Exceptions.Exception_Message (Exc));
4473+
Dump (Tree, "| ");
4474+
end if;
4475+
return False;
4476+
end SCOs_Nested_And_Ordered;
4477+
43654478
------------------------
43664479
-- Set_Scope_Entities --
43674480
------------------------
@@ -4375,7 +4488,14 @@ package body SC_Obligations is
43754488
-- Scopes are supposed to be set only once per compilation unit
43764489

43774490
pragma Assert (SE.Is_Empty);
4491+
4492+
pragma Assert (SCOs_Nested_And_Ordered (Scope_Entities));
43784493
SE := Scope_Entities;
4494+
4495+
if Verbose then
4496+
Put_Line ("Setting scopes for " & Image (CU) & ":");
4497+
Dump (SE, Line_Prefix => "| ");
4498+
end if;
43794499
end Set_Scope_Entities;
43804500

43814501
-------------------------------

0 commit comments

Comments
 (0)