1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363 | ------------------------------------------------------------------------------
-- --
-- TGen --
-- --
-- Copyright (C) 2023, AdaCore --
-- --
-- TGen is free software; you can redistribute it and/or modify it under --
-- under terms of the GNU General Public License as published by the --
-- Free Software Foundation; either version 3, or (at your option) any --
-- later version. This software is distributed in the hope that it will be --
-- useful but WITHOUT ANY WARRANTY; without even the implied warranty of --
-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. --
-- --
-- As a special exception under Section 7 of GPL version 3, you are --
-- granted additional permissions described in the GCC Runtime Library --
-- Exception, version 3.1, as published by the Free Software Foundation. --
-- --
-- You should have received a copy of the GNU General Public License and a --
-- copy of the GCC Runtime Library Exception along with this program; see --
-- the files COPYING3 and COPYING.RUNTIME respectively. If not, see --
-- <http://www.gnu.org/licenses/>. --
------------------------------------------------------------------------------
with Ada.Containers.Ordered_Sets;
with Ada.Containers.Vectors;
with Libadalang.Common; use Libadalang.Common;
with TGen.LAL_Utils; use TGen.LAL_Utils;
with TGen.Strings; use TGen.Strings;
package body TGen.Wrappers is
-- When dealing with preconditions, we end up with a DNF formula. We
-- represent it as a list of conjunctive clauses, i.e. conjunction of
-- literals where each literal is an atom or its negation.
type Literal is record
Neg : Boolean;
Value : Unbounded_String;
end record;
function "<" (L, R : Literal) return Boolean is
(if L.Neg = R.Neg
then L.Value < R.Value
else L.Neg < R.Neg);
function "=" (L, R : Literal) return Boolean is
(L.Neg = R.Neg and then L.Value = R.Value);
package Literal_Sets is new Ada.Containers.Ordered_Sets (Literal);
package Literal_Set_Vectors is new Ada.Containers.Vectors
(Index_Type => Positive,
Element_Type => Literal_Sets.Set,
"=" => Literal_Sets."=");
subtype Formula_Type is Literal_Set_Vectors.Vector;
type Polarity_Kind is new Boolean;
Dnf_Kind : constant Polarity_Kind := True;
Dnf_Neg_Kind : constant Polarity_Kind := False;
function Dnf
(E : Expr;
Polarity : Polarity_Kind := Dnf_Kind) return Formula_Type;
-- Return the DNF for a precondition expression. The Polarity parameter
-- is there to propagate the negation to literals (and puts (not E) in
-- DNF).
function Subprogram_Wrapper_Specification (F : Function_Typ) return String;
-- Return the code for the wrapper specification
procedure Write_Wrapper
(F_Body : File_Type;
Call_To_Orig_Subp : String;
Formula : Formula_Type);
function Subp_Kind (F : Function_Typ) return Ada_Subp_Kind is
(if F.Ret_Typ.Is_Null
then Ada_Subp_Kind_Procedure
else Ada_Subp_Kind_Function);
---------
-- Dnf --
---------
function Dnf
(E : Expr;
Polarity : Polarity_Kind := Dnf_Kind) return Formula_Type
is
Result : Formula_Type;
begin
case Kind (E) is
when Ada_Un_Op =>
case Kind (E.As_Un_Op.F_Op) is
when Ada_Op_Not =>
return Dnf (E.As_Un_Op.F_Expr, not Polarity);
when others =>
null;
end case;
when Ada_Bin_Op =>
declare
As_Bin_Op : constant Bin_Op := E.As_Bin_Op;
Ada_Op : constant Ada_Node_Kind_Type :=
Kind (As_Bin_Op.F_Op);
begin
case Ada_Op is
when Ada_Op_And_Then
| Ada_Op_And
| Ada_Op_Or_Else
| Ada_Op_Or
=>
declare
Dnf_Left : constant Formula_Type :=
Dnf (As_Bin_Op.F_Left, Polarity);
Dnf_Right : constant Formula_Type :=
Dnf (As_Bin_Op.F_Right, Polarity);
begin
-- Depending on the polarity: we are either building
-- a DNF, or a CNF, distribute respectively the "and"
-- operator, or the "or" operator.
if (Polarity = Dnf_Kind
and then Ada_Op in Ada_Op_And_Then | Ada_Op_And)
or else
(Polarity = Dnf_Neg_Kind
and then Ada_Op in Ada_Op_Or_Else | Ada_Op_Or)
then
for Clause_Left of Dnf_Left loop
for Clause_Right of Dnf_Right loop
Result.Append
(Clause_Left.Union (Clause_Right));
end loop;
end loop;
else
Result.Append (Dnf_Left);
Result.Append (Dnf_Right);
end if;
return Result;
end;
when others =>
null;
end case;
end;
when Ada_Paren_Expr =>
-- Do not unwrap the Paren_Expr if is is legally required by the
-- parenthesized expression, such as if-expressions or quantified
-- expressions.
if E.As_Paren_Expr.F_Expr.Kind not in
Ada_Cond_Expr
| Ada_Quantified_Expr
| Ada_Decl_Expr
then
return Dnf (E.As_Paren_Expr.F_Expr, Polarity);
end if;
when others =>
null;
end case;
Result.Append
(Literal_Sets.To_Set
(Literal'
(Neg => not Boolean (Polarity),
Value => To_Unbounded_String (+E.Text))));
return Result;
end Dnf;
-------------------
-- Write_Wrapper --
-------------------
procedure Write_Wrapper
(F_Body : File_Type;
Call_To_Orig_Subp : String;
Formula : Formula_Type)
is
use type Literal_Sets.Set;
Indent : constant String := " ";
begin
for Literal_Set of Formula loop
if Literal_Set = Formula.First_Element then
Put (F_Body, Indent & "if ");
else
Put (F_Body, Indent & "elsif ");
end if;
for Literal of Literal_Set loop
if Literal /= Literal_Set.First_Element then
Put (F_Body, "and then ");
end if;
if Literal.Neg then
Put (F_Body, "not ");
end if;
Put (F_Body, +Literal.Value & " ");
end loop;
Put_Line (F_Body, " then");
Put_Line (F_Body, Indent & " " & Call_To_Orig_Subp);
end loop;
end Write_Wrapper;
--------------------------------------
-- Subprogram_Wrapper_Specification --
--------------------------------------
function Subprogram_Wrapper_Specification (F : Function_Typ) return String
is
Kind : constant Ada_Subp_Kind := Subp_Kind (F);
Result : Unbounded_String;
begin
declare
begin
case Kind is
when Ada_Subp_Kind_Procedure =>
Append (Result, "procedure ");
when Ada_Subp_Kind_Function =>
Append (Result, "function ");
end case;
Append (Result, F.Simple_Name);
-- Then, deal with the parameters
if not F.Param_Order.Is_Empty then
Append (Result, "(");
for Param_Name of F.Param_Order loop
declare
Param_Type : constant SP.Ref :=
F.Component_Types.Element (Param_Name);
begin
Append (Result, Param_Name);
Append (Result, " : ");
Append
(Result, Image (F.Param_Modes.Element (Param_Name)) & " ");
Append (Result, Param_Type.Get.FQN & " ");
if Param_Name /= F.Param_Order.Last_Element then
Append (Result, " ; ");
end if;
end;
end loop;
Append (Result, ")");
end if;
-- Then, deal with the return type expression if this is a function
if Kind = Ada_Subp_Kind_Function then
Append (Result, " return ");
Append (Result, To_Ada (F.Ret_Typ.Get.Name));
end if;
return To_String (Result);
end;
end Subprogram_Wrapper_Specification;
-------------------------------------
-- Generate_Wrapper_For_Subprogram --
-------------------------------------
procedure Generate_Wrapper_For_Subprogram
(F_Spec, F_Body : File_Type;
Subprogram : Function_Typ;
Precond : Ada_Node;
Templates_Root_Dir : String)
is
use type Ada.Containers.Count_Type;
Subp_Spec_String : constant String :=
Subprogram_Wrapper_Specification (Subprogram);
-- String representation of the wrapper specification, e.g.
-- "procedure Foo (I : Integer)".
Call_To_User_Subp : Unbounded_String;
-- Call to the original user subprogram
Local_Package_Name : Ada_Qualified_Name;
-- Name of the subprogram in its compilation unit. This is its fully
-- qualified name, from which the compilation unit's fully qualified
-- name has been removed.
begin
-- Compute local name. Do not take into account the last element as this
-- is its hash.
for I in
Subprogram.Last_Comp_Unit_Idx + 1 .. Subprogram.Name.Last_Index - 1
loop
Local_Package_Name.Append (Subprogram.Name.Element (I));
end loop;
-- Compute the call to the original function
case Subp_Kind (Subprogram) is
when Ada_Subp_Kind_Function =>
Append (Call_To_User_Subp, "return ");
when Ada_Subp_Kind_Procedure =>
null;
end case;
Append
(Call_To_User_Subp,
Source_Package_Renaming & "." & To_Ada (Local_Package_Name));
if Subprogram.Param_Order.Length > 0 then
Append (Call_To_User_Subp, " (");
end if;
for Param_Name of Subprogram.Param_Order loop
Append (Call_To_User_Subp, Param_Name);
if Param_Name /= Subprogram.Param_Order.Last_Element then
Append (Call_To_User_Subp, ", ");
end if;
end loop;
if Subprogram.Param_Order.Length > 0 then
Append (Call_To_User_Subp, ");");
end if;
-- Declare the wrapper specification in the spec package
Put_Line (F_Spec, Subp_Spec_String & ";");
-- ... and in the body
Put_Line (F_Body, " " & Subp_Spec_String & " is");
Put_Line (F_Body, " begin");
-- Check whether there is a precondition attached to this subprogram
if not Precond.Is_Null then
declare
-- Get the formula for the precondition
F : constant Formula_Type := Dnf (Precond.As_Expr);
begin
-- Then, write the wrapper
Write_Wrapper
(F_Body => F_Body,
Call_To_Orig_Subp => +Call_To_User_Subp,
Formula => F);
-- Don't forget to write the last else case, which is the
-- Precondition_Error case.
Put_Line (F_Body, " else");
Put_Line (F_Body, " raise TGen.Precondition_Error;");
Put_Line (F_Body, " end if;");
end;
else
Put_Line (F_Body, " " & (+Call_To_User_Subp));
end if;
Put_Line (F_Body, " end " & Subprogram.Simple_Name & ";");
New_Line (F_Body);
end Generate_Wrapper_For_Subprogram;
end TGen.Wrappers;
|