Skip to content

Commit 645c41a

Browse files
martin-csmartin-cs
authored
Merge pull request #338 from tjj2017/translate_withed_units_once_only
Translate withed units once only
2 parents ec134c3 + 169f177 commit 645c41a

File tree

18 files changed

+167
-103
lines changed

18 files changed

+167
-103
lines changed

‎experiments/golden-results/StratoX-summary.txt

Lines changed: 17 additions & 52 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ Calling function: Process_Declaration
33
Error message: size clause not applied by the front-end
44
Nkind: N_Attribute_Definition_Clause
55
--
6-
Occurs: 379 times
6+
Occurs: 378 times
77
Calling function: Process_Pragma_Declaration
88
Error message: Unsupported pragma: Precondition
99
Nkind: N_Pragma
@@ -13,7 +13,7 @@ Calling function: Process_Declaration
1313
Error message: Unknown declaration kind
1414
Nkind: N_Validate_Unchecked_Conversion
1515
--
16-
Occurs: 153 times
16+
Occurs: 152 times
1717
Calling function: Process_Pragma_Declaration
1818
Error message: Unsupported pragma: Postcondition
1919
Nkind: N_Pragma
@@ -33,33 +33,33 @@ Calling function: Do_Expression
3333
Error message: Index of string unsupported
3434
Nkind: N_Indexed_Component
3535
--
36-
Occurs: 14 times
37-
Calling function: Process_Pragma_Declaration
38-
Error message: Unsupported pragma: Global
39-
Nkind: N_Pragma
40-
--
4136
Occurs: 13 times
4237
Calling function: Do_Expression
4338
Error message: Last of string unsupported
4439
Nkind: N_Attribute_Reference
4540
--
41+
Occurs: 13 times
42+
Calling function: Process_Pragma_Declaration
43+
Error message: Unsupported pragma: Global
44+
Nkind: N_Pragma
45+
--
4646
Occurs: 10 times
4747
Calling function: Do_Expression
4848
Error message: ATTRIBUTE_MACHINE unsupported
4949
Nkind: N_Attribute_Reference
5050
--
51-
Occurs: 10 times
52-
Calling function: Process_Pragma_Declaration
53-
Error message: Unsupported pragma: Check
54-
Nkind: N_Pragma
55-
--
5651
Occurs: 8 times
5752
Calling function: Do_Type_Reference
5853
Error message: Type of type not a type
5954
Nkind: N_Defining_Identifier
6055
--
6156
Occurs: 8 times
6257
Calling function: Process_Pragma_Declaration
58+
Error message: Unsupported pragma: Check
59+
Nkind: N_Pragma
60+
--
61+
Occurs: 8 times
62+
Calling function: Process_Pragma_Declaration
6363
Error message: Unsupported pragma: Obsolescent
6464
Nkind: N_Pragma
6565
--
@@ -74,11 +74,6 @@ Error message: Unknown pragma: ghost
7474
Nkind: N_Pragma
7575
--
7676
Occurs: 3 times
77-
Calling function: Do_Constant
78-
Error message: Unsupported constant type
79-
Nkind: N_Integer_Literal
80-
--
81-
Occurs: 3 times
8277
Calling function: Process_Declaration
8378
Error message: Address representation clauses are not currently supported
8479
Nkind: N_Attribute_Definition_Clause
@@ -114,9 +109,9 @@ Error message: unsupported lower range kind
114109
Nkind: N_Real_Literal
115110
--
116111
Occurs: 1 times
117-
Calling function: Do_Expression
118-
Error message: ATTRIBUTE_MACHINE_RADIX unsupported
119-
Nkind: N_Attribute_Reference
112+
Calling function: Do_Constant
113+
Error message: Unsupported constant type
114+
Nkind: N_Integer_Literal
120115
--
121116
Occurs: 1 times
122117
Calling function: Do_Expression
@@ -1718,11 +1713,6 @@ Occurs: 10 times
17181713
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:495 |
17191714
Error detected at REDACTED
17201715
--
1721-
Occurs: 8 times
1722-
+===========================GNAT BUG DETECTED==============================+
1723-
| GNU Ada (ada2goto) Constraint_Error Symbol_Table_Info.Symbol_Maps.Constant_Reference: key not in map|
1724-
Error detected at REDACTED
1725-
--
17261716
Occurs: 7 times
17271717
+===========================GNAT BUG DETECTED==============================+
17281718
| GNU Ada (ada2goto) Assert_Failure failed precondition from goto_utils.ads:147|
@@ -1743,9 +1733,9 @@ Occurs: 3 times
17431733
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:495 |
17441734
Error detected at REDACTED
17451735
--
1746-
Occurs: 3 times
1736+
Occurs: 2 times
17471737
+===========================GNAT BUG DETECTED==============================+
1748-
| GNU Ada (ada2goto) Assert_Failure tree_walk.adb:998 |
1738+
| GNU Ada (ada2goto) Constraint_Error Symbol_Table_Info.Symbol_Maps.Constant_Reference: key not in map|
17491739
Error detected at REDACTED
17501740
--
17511741
Occurs: 2 times
@@ -2203,35 +2193,10 @@ Occurs: 1 times
22032193
| GNU Ada (ada2goto) Assert_Failure sinfo.adb:394 |
22042194
Error detected at REDACTED
22052195
--
2206-
Occurs: 1 times
2207-
+===========================GNAT BUG DETECTED==============================+
2208-
| GNU Ada (ada2goto) Constraint_Error Symbol_Table_Info.Symbol_Maps.Constant_Reference: key not in map|
2209-
Error detected at REDACTED
2210-
--
2211-
Occurs: 1 times
2212-
+===========================GNAT BUG DETECTED==============================+
2213-
| GNU Ada (ada2goto) Constraint_Error Symbol_Table_Info.Symbol_Maps.Constant_Reference: key not in map|
2214-
Error detected at REDACTED
2215-
--
2216-
Occurs: 1 times
2217-
+===========================GNAT BUG DETECTED==============================+
2218-
| GNU Ada (ada2goto) Constraint_Error Symbol_Table_Info.Symbol_Maps.Constant_Reference: key not in map|
2219-
Error detected at REDACTED
2220-
--
2221-
Occurs: 1 times
2222-
+===========================GNAT BUG DETECTED==============================+
2223-
| GNU Ada (ada2goto) Constraint_Error Symbol_Table_Info.Symbol_Maps.Constant_Reference: key not in map|
2224-
Error detected at REDACTED
2225-
--
22262196
Occurs: 25 times
22272197
<========================>
22282198
raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from goto_utils.ads:147
22292199

2230-
--
2231-
Occurs: 2 times
2232-
<========================>
2233-
raised CONSTRAINT_ERROR : Symbol_Table_Info.Symbol_Maps.Constant_Reference: key not in map
2234-
22352200
--
22362201
Occurs: 2 times
22372202
<========================>

‎experiments/golden-results/Tokeneer-summary.txt

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1030,7 +1030,7 @@ Error detected at REDACTED
10301030
--
10311031
Occurs: 2 times
10321032
+===========================GNAT BUG DETECTED==============================+
1033-
| GNU Ada (ada2goto) Assert_Failure failed precondition from tree_walk.ads:109|
1033+
| GNU Ada (ada2goto) Assert_Failure failed precondition from tree_walk.ads:108|
10341034
Error detected at REDACTED
10351035
--
10361036
Occurs: 1 times
@@ -1100,17 +1100,17 @@ Error detected at REDACTED
11001100
--
11011101
Occurs: 1 times
11021102
+===========================GNAT BUG DETECTED==============================+
1103-
| GNU Ada (ada2goto) Assert_Failure failed precondition from tree_walk.ads:109|
1103+
| GNU Ada (ada2goto) Assert_Failure failed precondition from tree_walk.ads:108|
11041104
Error detected at REDACTED
11051105
--
11061106
Occurs: 1 times
11071107
+===========================GNAT BUG DETECTED==============================+
1108-
| GNU Ada (ada2goto) Assert_Failure failed precondition from tree_walk.ads:109|
1108+
| GNU Ada (ada2goto) Assert_Failure failed precondition from tree_walk.ads:108|
11091109
Error detected at REDACTED
11101110
--
11111111
Occurs: 1 times
11121112
+===========================GNAT BUG DETECTED==============================+
1113-
| GNU Ada (ada2goto) Assert_Failure failed precondition from tree_walk.ads:109|
1113+
| GNU Ada (ada2goto) Assert_Failure failed precondition from tree_walk.ads:108|
11141114
Error detected at REDACTED
11151115
--
11161116
Occurs: 1 times

‎experiments/golden-results/muen-summary.txt

Lines changed: 1 addition & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -99,11 +99,6 @@ Error message: Unhandled aggregate kind: E_RECORD_TYPE_WITH_PRIVATE
9999
Nkind: N_Aggregate
100100
--
101101
Occurs: 1 times
102-
Calling function: Do_Constant
103-
Error message: Unsupported constant type
104-
Nkind: N_Integer_Literal
105-
--
106-
Occurs: 1 times
107102
Calling function: Do_Expression
108103
Error message: ATTRIBUTE_MIN unsupported
109104
Nkind: N_Attribute_Reference
@@ -2973,11 +2968,6 @@ Occurs: 3 times
29732968
| GNU Ada (ada2goto) Assert_Failure failed precondition from goto_utils.ads:147|
29742969
Error detected at REDACTED
29752970
--
2976-
Occurs: 3 times
2977-
+===========================GNAT BUG DETECTED==============================+
2978-
| GNU Ada (ada2goto) Constraint_Error Symbol_Table_Info.Symbol_Maps.Constant_Reference: key not in map|
2979-
Error detected at REDACTED
2980-
--
29812971
Occurs: 2 times
29822972
+===========================GNAT BUG DETECTED==============================+
29832973
| GNU Ada (ada2goto) Assert_Failure failed precondition from ireps.ads:1784|
@@ -3185,7 +3175,7 @@ Error detected at REDACTED
31853175
--
31863176
Occurs: 1 times
31873177
+===========================GNAT BUG DETECTED==============================+
3188-
| GNU Ada (ada2goto) Assert_Failure failed precondition from tree_walk.ads:109|
3178+
| GNU Ada (ada2goto) Assert_Failure failed precondition from tree_walk.ads:108|
31893179
Error detected at REDACTED
31903180
--
31913181
Occurs: 1 times

‎gnat2goto/driver/driver.adb

Lines changed: 30 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -353,14 +353,18 @@ package body Driver is
353353
is
354354
pragma Assert (Nkind (GNAT_Root) = N_Compilation_Unit);
355355

356-
Unit_Is_Subprogram : Boolean;
357356
Program_Symbol : constant Symbol :=
358-
Do_Compilation_Unit (GNAT_Root, Unit_Is_Subprogram);
357+
Do_Compilation_Unit (GNAT_Root);
359358

360-
-- Only add CPROVER_Start if the unit is subprogram and the user did not
361-
-- suppress it (by cmdl option).
359+
The_Unit : constant Node_Id := Unit (GNAT_Root);
360+
361+
Unit_Name : constant Symbol_Id :=
362+
Intern (Unique_Name (Unique_Defining_Entity (The_Unit)));
363+
364+
-- Only add CPROVER_Start if the unit is subprogram body
365+
-- and the user did not suppress it (by cmdl option).
362366
Add_Start : constant Boolean :=
363-
Unit_Is_Subprogram and not Suppress_Cprover_Start;
367+
Nkind (The_Unit) = N_Subprogram_Body and not Suppress_Cprover_Start;
364368

365369
Sym_Tab_File : File_Type;
366370
Base_Name : constant String :=
@@ -369,6 +373,27 @@ package body Driver is
369373

370374
Sanitised_Symbol_Table : Symbol_Table;
371375
begin
376+
if Nkind (The_Unit) not in N_Subprogram_Body | N_Package_Body or else
377+
not Global_Symbol_Table.Contains (Unit_Name)
378+
then
379+
-- Only non-generic compilation unit bodies generate a
380+
-- json symbol table. Generic declarations and their bodies
381+
-- do not generate json symbol tables because instances of the
382+
-- generic units are expanded in the AST by the front-end.
383+
-- Library level generic instantiations, although they are
384+
-- declarations, appear in the tree as unit bodies, and so
385+
-- gnat2goto will generate a json symbol for such instantiations
386+
-- As generic declarations are not translated by Do_Compilation_Unit
387+
-- they will not have an entry in the symbol table.
388+
-- Hence a unit body which does not have an entry in the
389+
-- global symbol table is a generic body and a
390+
-- json symbol table is not generated.
391+
return;
392+
end if;
393+
394+
-- The compilation unit is a body, a tranlation has been completed
395+
-- and the symbol table populated.
396+
-- Now generate the json file from the symbol table
372397
Create (Sym_Tab_File, Out_File, Base_Name & ".json_symtab");
373398
-- Gather local symbols and put them in the symtab
374399
declare

‎gnat2goto/driver/tree_walk.adb

Lines changed: 38 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -960,10 +960,9 @@ package body Tree_Walk is
960960
-- Do_Compilation_Unit --
961961
-------------------------
962962

963-
function Do_Compilation_Unit (N : Node_Id; Unit_Is_Subprogram : out Boolean)
964-
return Symbol
963+
function Do_Compilation_Unit (N : Node_Id) return Symbol
965964
is
966-
U : constant Node_Id := Unit (N);
965+
U : constant Node_Id := Unit (N);
967966
Unit_Name : constant Symbol_Id :=
968967
Intern (Unique_Name (Unique_Defining_Entity (U)));
969968
Unit_Symbol : Symbol;
@@ -974,31 +973,45 @@ package body Tree_Walk is
974973

975974
case Nkind (U) is
976975
when N_Subprogram_Body =>
977-
-- The specification of the subprogram body has already
978-
-- been inserted into the symbol table by the call to
979-
-- Do_Withed_Unit_Specs.
980-
pragma Assert (Global_Symbol_Table.Contains (Unit_Name));
981-
Unit_Symbol := Global_Symbol_Table (Unit_Name);
982-
983-
-- Now compile the body of the subprogram
984-
Unit_Symbol.Value := Do_Subprogram_Or_Block (U);
976+
-- If the unit is not the body of a generic declaration,
977+
-- the subprogram specification will have been entered into the
978+
-- symbol table by the processing of with'd units including
979+
-- the specification of this unit.
980+
-- Now the subprogram's body is added to the symbol table.
981+
if Global_Symbol_Table.Contains (Unit_Name) then
982+
Unit_Symbol := Global_Symbol_Table (Unit_Name);
983+
Unit_Symbol.Value := Do_Subprogram_Or_Block (U);
985984

986-
-- and update the symbol table entry for this subprogram.
987-
Global_Symbol_Table.Replace (Unit_Name, Unit_Symbol);
988-
Unit_Is_Subprogram := True;
985+
-- and update the symbol table entry for this subprogram.
986+
Global_Symbol_Table.Replace (Unit_Name, Unit_Symbol);
987+
else
988+
-- It is the body of a generic declaration and the
989+
-- and generic declarations are not translated.
990+
-- Gnat2goto does not tranlate the body either snd
991+
-- so there is nothing to be done.
992+
null;
993+
end if;
989994

990995
when N_Package_Body =>
991-
declare
992-
Dummy : constant Irep := Do_Subprogram_Or_Block (U);
993-
pragma Unreferenced (Dummy);
994-
begin
995-
-- The specification of the package body has already
996+
-- If the unit is not the body of a generic declaration,
997+
-- the specification of the package body has already
996998
-- been inserted into the symbol table by the call to
997999
-- Do_Withed_Unit_Specs.
998-
pragma Assert (Global_Symbol_Table.Contains (Unit_Name));
999-
Unit_Symbol := Global_Symbol_Table (Unit_Name);
1000-
Unit_Is_Subprogram := False;
1001-
end;
1000+
if Global_Symbol_Table.Contains (Unit_Name) then
1001+
declare
1002+
Dummy : constant Irep := Do_Subprogram_Or_Block (U);
1003+
pragma Unreferenced (Dummy);
1004+
begin
1005+
Unit_Symbol := Global_Symbol_Table (Unit_Name);
1006+
end;
1007+
else
1008+
-- It is the body of a generic declaration and the
1009+
-- and generic declarations are not translated.
1010+
-- Gnat2goto does not tranlate the body either snd
1011+
-- so there is nothing to be done.
1012+
null;
1013+
end if;
1014+
10021015
when N_Subprogram_Declaration | N_Package_Declaration =>
10031016
-- Package and subprogram declarations are processed
10041017
-- when they appear in a with statement.
@@ -1009,15 +1022,15 @@ package body Tree_Walk is
10091022
-- think such uses would be unusual (TJJ 21/11/2019)
10101023
null;
10111024
when N_Generic_Subprogram_Declaration
1012-
| N_Generic_Package_Declaration =>
1025+
| N_Generic_Package_Declaration =>
10131026
-- Generic subprograms and packages
10141027
-- don't need to specially handled
10151028
-- because their instantiations appear as nodes
10161029
-- in the AST
10171030
null;
10181031
when others =>
10191032
Report_Unhandled_Node_Empty (N, "Do_Compilation_Unit",
1020-
"Generic units are unsupported");
1033+
"unsupported compilation unit sort");
10211034
end case;
10221035

10231036
return Unit_Symbol;

‎gnat2goto/driver/tree_walk.ads

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -75,8 +75,7 @@ package Tree_Walk is
7575

7676
Check_Function_Symbol : Irep := Ireps.Empty;
7777

78-
function Do_Compilation_Unit (N : Node_Id; Unit_Is_Subprogram : out Boolean)
79-
return Symbol
78+
function Do_Compilation_Unit (N : Node_Id) return Symbol
8079
with Pre => Nkind (N) = N_Compilation_Unit;
8180

8281
function Do_Type_Reference (E : Entity_Id) return Irep

0 commit comments

Comments
 (0)