Skip to content

Commit f1849db

Browse files
martin-csmartin-cs
authored
Merge pull request #349 from tjj2017/address_model
Address model
2 parents e81b928 + 60f7e8f commit f1849db

File tree

21 files changed

+531
-47
lines changed

21 files changed

+531
-47
lines changed

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

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ Calling function: Process_Pragma_Declaration
88
Error message: Unsupported pragma: Precondition
99
Nkind: N_Pragma
1010
--
11-
Occurs: 232 times
11+
Occurs: 231 times
1212
Calling function: Process_Declaration
1313
Error message: Unknown declaration kind
1414
Nkind: N_Validate_Unchecked_Conversion
@@ -1745,7 +1745,7 @@ Error detected at REDACTED
17451745
--
17461746
Occurs: 3 times
17471747
+===========================GNAT BUG DETECTED==============================+
1748-
| GNU Ada (ada2goto) Assert_Failure tree_walk.adb:999 |
1748+
| GNU Ada (ada2goto) Assert_Failure tree_walk.adb:998 |
17491749
Error detected at REDACTED
17501750
--
17511751
Occurs: 2 times
@@ -1760,6 +1760,11 @@ Error detected at REDACTED
17601760
--
17611761
Occurs: 1 times
17621762
+===========================GNAT BUG DETECTED==============================+
1763+
| GNU Ada (ada2goto) Assert_Failure atree.adb:992 |
1764+
Error detected at REDACTED
1765+
--
1766+
Occurs: 1 times
1767+
+===========================GNAT BUG DETECTED==============================+
17631768
| GNU Ada (ada2goto) Assert_Failure failed precondition from arrays.ads:71 |
17641769
Error detected at REDACTED
17651770
--
@@ -2160,7 +2165,7 @@ Error detected at REDACTED
21602165
--
21612166
Occurs: 1 times
21622167
+===========================GNAT BUG DETECTED==============================+
2163-
| GNU Ada (ada2goto) Assert_Failure failed precondition from tree_walk.adb:72|
2168+
| GNU Ada (ada2goto) Assert_Failure failed precondition from tree_walk.adb:71|
21642169
Error detected at REDACTED
21652170
--
21662171
Occurs: 1 times
@@ -2232,11 +2237,6 @@ Occurs: 2 times
22322237
<========================>
22332238
raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from arrays.ads:51
22342239

2235-
--
2236-
Occurs: 2 times
2237-
<========================>
2238-
raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from ireps.ads:1648
2239-
22402240
--
22412241
Occurs: 2 times
22422242
<========================>
@@ -2245,5 +2245,5 @@ raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from range_check.a
22452245
--
22462246
Occurs: 1 times
22472247
<========================>
2248-
raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from tree_walk.adb:72
2248+
raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from tree_walk.adb:71
22492249

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1035,7 +1035,7 @@ Error detected at REDACTED
10351035
--
10361036
Occurs: 2 times
10371037
+===========================GNAT BUG DETECTED==============================+
1038-
| GNU Ada (ada2goto) Assert_Failure failed precondition from tree_walk.ads:106|
1038+
| GNU Ada (ada2goto) Assert_Failure failed precondition from tree_walk.ads:109|
10391039
Error detected at REDACTED
10401040
--
10411041
Occurs: 1 times
@@ -1105,17 +1105,17 @@ 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:106|
1108+
| GNU Ada (ada2goto) Assert_Failure failed precondition from tree_walk.ads:109|
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:106|
1113+
| GNU Ada (ada2goto) Assert_Failure failed precondition from tree_walk.ads:109|
11141114
Error detected at REDACTED
11151115
--
11161116
Occurs: 1 times
11171117
+===========================GNAT BUG DETECTED==============================+
1118-
| GNU Ada (ada2goto) Assert_Failure failed precondition from tree_walk.ads:106|
1118+
| GNU Ada (ada2goto) Assert_Failure failed precondition from tree_walk.ads:109|
11191119
Error detected at REDACTED
11201120
--
11211121
Occurs: 1 times

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3185,7 +3185,7 @@ Error detected at REDACTED
31853185
--
31863186
Occurs: 1 times
31873187
+===========================GNAT BUG DETECTED==============================+
3188-
| GNU Ada (ada2goto) Assert_Failure failed precondition from tree_walk.ads:106|
3188+
| GNU Ada (ada2goto) Assert_Failure failed precondition from tree_walk.ads:109|
31893189
Error detected at REDACTED
31903190
--
31913191
Occurs: 1 times

‎gnat2goto/driver/asvat-address_model.adb

Lines changed: 170 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,170 @@
1+
with GOTO_Utils; use GOTO_Utils;
2+
with Nlists; use Nlists;
3+
with Tree_Walk; use Tree_Walk;
4+
with Sem_Util; use Sem_Util;
5+
with Einfo; use Einfo;
6+
with Namet; use Namet;
7+
with Follow; use Follow;
8+
package body ASVAT.Address_Model is
9+
10+
-------------------------
11+
-- Do_ASVAT_Address_Of --
12+
-------------------------
13+
14+
function Do_ASVAT_Address_Of (N : Node_Id) return Irep is
15+
begin
16+
return Make_Op_Typecast
17+
(Op0 => Do_Address_Of (N),
18+
Source_Location => Get_Source_Location (N),
19+
I_Type => Make_Pointer_Type
20+
(I_Subtype => Make_Unsignedbv_Type (8),
21+
Width => Pointer_Type_Width),
22+
Range_Check => False);
23+
end Do_ASVAT_Address_Of;
24+
25+
------------------------------------
26+
-- Get_Intrinsic_Address_Function -
27+
------------------------------------
28+
29+
function Get_Intrinsic_Address_Function (E : Entity_Id) return
30+
Address_To_Access_Functions
31+
is
32+
Fun_Name : constant String := Get_Name_String (Chars (E));
33+
begin
34+
return (if Fun_Name = "to_pointer" then
35+
To_Pointer_Function
36+
elsif Fun_Name = "to_address" then
37+
To_Address_Function
38+
else
39+
Not_An_Address_Function);
40+
end Get_Intrinsic_Address_Function;
41+
42+
---------------------
43+
-- Make_To_Pointer --
44+
---------------------
45+
46+
procedure Make_To_Pointer (E : Entity_Id) is
47+
Address_Parameter : constant Node_Id :=
48+
First (Parameter_Specifications (Declaration_Node (E)));
49+
begin
50+
pragma Assert ((Present (Address_Parameter) and
51+
not Present (Next (Address_Parameter)))
52+
and then not Out_Present (Address_Parameter)
53+
and then
54+
Nkind (Parameter_Type (Address_Parameter)) in N_Has_Etype
55+
and then
56+
Unique_Name
57+
(Etype (Parameter_Type (Address_Parameter))) =
58+
"system__address",
59+
"The function To_Pointer must have a single in mode " &
60+
"parameter of type System.Address");
61+
62+
declare
63+
Source_Location : constant Irep := Get_Source_Location (E);
64+
Function_Name : constant String := Unique_Name (E);
65+
Function_Id : constant Symbol_Id := Intern (Function_Name);
66+
Function_Type : constant Node_Id := Etype (E);
67+
68+
Param_Name : constant String :=
69+
Unique_Name (Defining_Identifier (Address_Parameter));
70+
71+
Param_Type : constant Irep :=
72+
Do_Type_Reference (Etype (Parameter_Type (Address_Parameter)));
73+
74+
Param_Irep : constant Irep :=
75+
Make_Symbol_Expr
76+
(Source_Location => Get_Source_Location (Address_Parameter),
77+
I_Type => Param_Type,
78+
Range_Check => False,
79+
Identifier => Param_Name);
80+
81+
Return_Type : constant Irep := Follow_Symbol_Type
82+
(Do_Type_Reference (Function_Type), Global_Symbol_Table);
83+
84+
Return_Statement : constant Irep :=
85+
Make_Code_Return
86+
(Return_Value => Make_Op_Typecast
87+
(Op0 => Param_Irep,
88+
Source_Location => Source_Location,
89+
I_Type => Return_Type),
90+
Source_Location => Source_Location,
91+
I_Type => Return_Type,
92+
Range_Check => False);
93+
94+
Function_Body : constant Irep := Make_Code_Block (Source_Location);
95+
96+
Function_Symbol : Symbol := Global_Symbol_Table (Function_Id);
97+
begin
98+
Append_Op (Function_Body, Return_Statement);
99+
100+
Function_Symbol.Value := Function_Body;
101+
Global_Symbol_Table.Replace (Function_Id, Function_Symbol);
102+
end;
103+
end Make_To_Pointer;
104+
105+
---------------------
106+
-- To_Address --
107+
---------------------
108+
109+
procedure Make_To_Address (E : Entity_Id) is
110+
Pointer_Parameter : constant Node_Id :=
111+
First (Parameter_Specifications (Declaration_Node (E)));
112+
Function_Type : constant Node_Id := Etype (E);
113+
begin
114+
pragma Assert ((Present (Pointer_Parameter) and
115+
not Present (Next (Pointer_Parameter)))
116+
and then not Out_Present (Pointer_Parameter)
117+
and then
118+
Kind (Do_Type_Reference
119+
(Etype (Parameter_Type (Pointer_Parameter)))) =
120+
I_Pointer_Type
121+
and then Unique_Name (Function_Type) = "system__address",
122+
"The function To_Address must have a single in mode " &
123+
"parameter of an access type");
124+
125+
declare
126+
Source_Location : constant Irep := Get_Source_Location (E);
127+
Function_Name : constant String := Unique_Name (E);
128+
Function_Id : constant Symbol_Id := Intern (Function_Name);
129+
130+
Param_Name : constant String :=
131+
Unique_Name (Defining_Identifier (Pointer_Parameter));
132+
133+
Param_Type : constant Irep :=
134+
Do_Type_Reference (Etype (Parameter_Type (Pointer_Parameter)));
135+
136+
Param_Irep : constant Irep :=
137+
Make_Symbol_Expr
138+
(Source_Location => Get_Source_Location (Pointer_Parameter),
139+
I_Type => Param_Type,
140+
Range_Check => False,
141+
Identifier => Param_Name);
142+
143+
Return_Type : constant Irep := Make_Pointer_Type
144+
(I_Subtype => Make_Unsignedbv_Type (8),
145+
Width => Pointer_Type_Width);
146+
147+
Return_Statement : constant Irep :=
148+
Make_Code_Return
149+
(Return_Value => Make_Op_Typecast
150+
(Op0 => Param_Irep,
151+
Source_Location => Source_Location,
152+
I_Type => Return_Type,
153+
Range_Check => False),
154+
Source_Location => Source_Location,
155+
I_Type => Return_Type,
156+
Range_Check => False);
157+
158+
Function_Body : constant Irep := Make_Code_Block (Source_Location);
159+
160+
Function_Symbol : Symbol := Global_Symbol_Table (Function_Id);
161+
begin
162+
Append_Op (Function_Body, Return_Statement);
163+
164+
Function_Symbol.Value := Function_Body;
165+
Global_Symbol_Table.Replace (Function_Id, Function_Symbol);
166+
end;
167+
168+
end Make_To_Address;
169+
170+
end ASVAT.Address_Model;

‎gnat2goto/driver/asvat-address_model.ads

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
with Types; use Types;
2+
with Atree; use Atree;
3+
with Sinfo; use Sinfo;
4+
with Snames; use Snames;
5+
with Ireps; use Ireps;
6+
package ASVAT.Address_Model is
7+
8+
type Address_To_Access_Functions is
9+
(Not_An_Address_Function, To_Pointer_Function, To_Address_Function);
10+
11+
function Do_ASVAT_Address_Of (N : Node_Id) return Irep
12+
with Pre => Nkind (N) = N_Attribute_Reference and then
13+
Get_Attribute_Id (Attribute_Name (N)) = Attribute_Address;
14+
15+
function Get_Intrinsic_Address_Function (E : Entity_Id) return
16+
Address_To_Access_Functions;
17+
18+
procedure Make_To_Pointer (E : Entity_Id);
19+
-- with Pre => Is_Intrinsic_Subprogram (E) and
20+
-- Get_Name_String (Chars (E)) = "to_pointer";
21+
22+
procedure Make_To_Address (E : Entity_Id);
23+
-- with Pre => Is_Intrinsic_Subprogram (E) and
24+
-- Get_Name_String (Chars (E)) = "to_address";
25+
end ASVAT.Address_Model;

‎gnat2goto/driver/asvat.ads

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
with Ada.Containers.Hashed_Maps;
2+
with Ada.Containers; use Ada.Containers;
3+
with GNATCOLL.Symbols;
4+
with Symbol_Table_Info; use Symbol_Table_Info;
5+
with Uintp; use Uintp;
6+
package ASVAT is
7+
private
8+
type Entity_Info is record
9+
Specified_Rep_Size : Uint;
10+
Specified_Rep_Component_Size : Uint;
11+
end record;
12+
13+
Empty_Entity_Info : constant Entity_Info :=
14+
(Specified_Rep_Size => Uint_0,
15+
Specified_Rep_Component_Size => Uint_0);
16+
17+
use type GNATCOLL.Symbols.Symbol; -- for "=" operator
18+
19+
package Entity_Info_Maps is new Hashed_Maps
20+
(Key_Type => Symbol_Id, -- Should be Entity_Id
21+
Element_Type => Entity_Info,
22+
Hash => GNATCOLL.Symbols.Hash,
23+
Equivalent_Keys => "=");
24+
25+
subtype Entity_Info_Table is Entity_Info_Maps.Map;
26+
27+
Extra_Entity_Info : Entity_Info_Table;
28+
end ASVAT;

‎gnat2goto/driver/goto_utils.ads

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -85,7 +85,7 @@ package GOTO_Utils is
8585
BaseName : String;
8686
Symbol_Type : Irep;
8787
A_Symbol_Table : in out Symbol_Table)
88-
with Pre => Kind (Symbol_Type) in Class_Type;
88+
with Pre => Kind (Symbol_Type) in Class_Type | I_Address_Of_Expr;
8989

9090
function New_Function_Symbol_Entry (Name : String; Symbol_Type : Irep;
9191
Value : Irep;

0 commit comments

Comments
 (0)