1
|
(********************************************************************)
|
2
|
(* *)
|
3
|
(* The LustreC compiler toolset / The LustreC Development Team *)
|
4
|
(* Copyright 2012 - -- ONERA - CNRS - INPT *)
|
5
|
(* *)
|
6
|
(* LustreC is free software, distributed WITHOUT ANY WARRANTY *)
|
7
|
(* under the terms of the GNU Lesser General Public License *)
|
8
|
(* version 2.1. *)
|
9
|
(* *)
|
10
|
(********************************************************************)
|
11
|
|
12
|
open Utils
|
13
|
open Lustre_types
|
14
|
open Corelang
|
15
|
open Format
|
16
|
|
17
|
(* To update thank to some command line options *)
|
18
|
let debug = ref false
|
19
|
|
20
|
(** Normalisation iters through the AST of expressions and bind fresh definition
|
21
|
when some criteria are met. This creation of fresh definition is performed by
|
22
|
the function mk_expr_alias_opt when the alias argument is on.
|
23
|
|
24
|
Initial expressions, ie expressions attached a variable in an equation
|
25
|
definition are not aliased. This non-alias feature is propagated in the
|
26
|
expression AST for array access and power construct, tuple, and some special
|
27
|
cases of arrows.
|
28
|
|
29
|
Two global variables may impact the normalization process:
|
30
|
- unfold_arrow_active
|
31
|
- force_alias_ite: when set, bind a fresh alias for then and else
|
32
|
definitions.
|
33
|
*)
|
34
|
|
35
|
type param_t = {
|
36
|
unfold_arrow_active : bool;
|
37
|
force_alias_ite : bool;
|
38
|
force_alias_internal_fun : bool;
|
39
|
}
|
40
|
|
41
|
let params =
|
42
|
ref
|
43
|
{
|
44
|
unfold_arrow_active = false;
|
45
|
force_alias_ite = false;
|
46
|
force_alias_internal_fun = false;
|
47
|
}
|
48
|
|
49
|
type norm_ctx_t = {
|
50
|
parentid : ident;
|
51
|
vars : var_decl list;
|
52
|
is_output : ident -> bool;
|
53
|
}
|
54
|
|
55
|
let expr_true loc ck =
|
56
|
{
|
57
|
expr_tag = Utils.new_tag ();
|
58
|
expr_desc = Expr_const (Const_tag tag_true);
|
59
|
expr_type = Type_predef.type_bool;
|
60
|
expr_clock = ck;
|
61
|
expr_delay = Delay.new_var ();
|
62
|
expr_annot = None;
|
63
|
expr_loc = loc;
|
64
|
}
|
65
|
|
66
|
let expr_false loc ck =
|
67
|
{
|
68
|
expr_tag = Utils.new_tag ();
|
69
|
expr_desc = Expr_const (Const_tag tag_false);
|
70
|
expr_type = Type_predef.type_bool;
|
71
|
expr_clock = ck;
|
72
|
expr_delay = Delay.new_var ();
|
73
|
expr_annot = None;
|
74
|
expr_loc = loc;
|
75
|
}
|
76
|
|
77
|
let expr_once loc ck =
|
78
|
{
|
79
|
expr_tag = Utils.new_tag ();
|
80
|
expr_desc = Expr_arrow (expr_true loc ck, expr_false loc ck);
|
81
|
expr_type = Type_predef.type_bool;
|
82
|
expr_clock = ck;
|
83
|
expr_delay = Delay.new_var ();
|
84
|
expr_annot = None;
|
85
|
expr_loc = loc;
|
86
|
}
|
87
|
|
88
|
let is_expr_once =
|
89
|
let dummy_expr_once = expr_once Location.dummy (Clocks.new_var true) in
|
90
|
fun expr -> Corelang.is_eq_expr expr dummy_expr_once
|
91
|
|
92
|
let unfold_arrow expr =
|
93
|
match expr.expr_desc with
|
94
|
| Expr_arrow (e1, e2) ->
|
95
|
let loc = expr.expr_loc in
|
96
|
let ck = List.hd (Clocks.clock_list_of_clock expr.expr_clock) in
|
97
|
{ expr with expr_desc = Expr_ite (expr_once loc ck, e1, e2) }
|
98
|
| _ -> assert false
|
99
|
|
100
|
(* Get the equation in [defs] with [expr] as rhs, if any *)
|
101
|
let get_expr_alias defs expr =
|
102
|
try
|
103
|
Some
|
104
|
(List.find
|
105
|
(fun eq ->
|
106
|
Clocks.equal expr.expr_clock eq.eq_rhs.expr_clock
|
107
|
&& is_eq_expr eq.eq_rhs expr)
|
108
|
defs)
|
109
|
with Not_found -> None
|
110
|
|
111
|
(* Replace [expr] with (tuple of) [locals] *)
|
112
|
let replace_expr locals expr =
|
113
|
match locals with
|
114
|
| [] -> assert false
|
115
|
| [ v ] ->
|
116
|
{ expr with expr_tag = Utils.new_tag (); expr_desc = Expr_ident v.var_id }
|
117
|
| _ ->
|
118
|
{
|
119
|
expr with
|
120
|
expr_tag = Utils.new_tag ();
|
121
|
expr_desc = Expr_tuple (List.map expr_of_vdecl locals);
|
122
|
}
|
123
|
|
124
|
(* IS IT USED ? TODO
|
125
|
(* Create an alias for [expr], if none exists yet *)
|
126
|
let mk_expr_alias (parentid, vars) (defs, vars) expr =
|
127
|
(*Format.eprintf "mk_expr_alias %a %a %a@." Printers.pp_expr expr Types.pp expr.expr_type Clocks.pp_ck expr.expr_clock;*)
|
128
|
match get_expr_alias defs expr with
|
129
|
| Some eq ->
|
130
|
let aliases = List.map (fun id -> List.find (fun v -> v.var_id = id) vars) eq.eq_lhs in
|
131
|
(defs, vars), replace_expr aliases expr
|
132
|
| None ->
|
133
|
let new_aliases =
|
134
|
List.map2
|
135
|
(mk_fresh_var (parentid, vars) expr.expr_loc)
|
136
|
(Types.type_list_of_type expr.expr_type)
|
137
|
(Clocks.clock_list_of_clock expr.expr_clock) in
|
138
|
let new_def =
|
139
|
mkeq expr.expr_loc (List.map (fun v -> v.var_id) new_aliases, expr)
|
140
|
in
|
141
|
(* Format.eprintf "Checking def of alias: %a -> %a@." (fprintf_list ~sep:", " (fun fmt v -> Format.pp_print_string fmt v.var_id)) new_aliases Printers.pp_expr expr; *)
|
142
|
(new_def::defs, new_aliases@vars), replace_expr new_aliases expr
|
143
|
*)
|
144
|
|
145
|
(* Create an alias for [expr], if [expr] is not already an alias (i.e. an ident)
|
146
|
and [opt] is true
|
147
|
|
148
|
|
149
|
*)
|
150
|
let mk_expr_alias_opt opt norm_ctx (defs, vars) expr =
|
151
|
if !debug then
|
152
|
Log.report ~plugin:"normalization" ~level:2 (fun fmt ->
|
153
|
Format.fprintf fmt "mk_expr_alias_opt %B %a %a %a@." opt
|
154
|
Printers.pp_expr expr Types.pp expr.expr_type Clocks.pp
|
155
|
expr.expr_clock);
|
156
|
match expr.expr_desc with
|
157
|
| Expr_ident _ -> (defs, vars), expr
|
158
|
| _ -> (
|
159
|
match get_expr_alias defs expr with
|
160
|
| Some eq ->
|
161
|
(* Format.eprintf "Found a preexisting definition@."; *)
|
162
|
let aliases =
|
163
|
List.map
|
164
|
(fun id -> List.find (fun v -> v.var_id = id) vars)
|
165
|
eq.eq_lhs
|
166
|
in
|
167
|
(defs, vars), replace_expr aliases expr
|
168
|
| None ->
|
169
|
(*
|
170
|
Format.eprintf "Didnt found a preexisting definition (opt=%b)@." opt;
|
171
|
* Format.eprintf "existing defs are: @[[%a@]]@."
|
172
|
* (fprintf_list ~sep:"@ "(fun fmt eq ->
|
173
|
* Format.fprintf fmt "ck:%a isckeq=%b, , iseq=%b, eq=%a"
|
174
|
* Clocks.pp_ck eq.eq_rhs.expr_clock
|
175
|
* (Clocks.eq_clock expr.expr_clock eq.eq_rhs.expr_clock)
|
176
|
* (is_eq_expr eq.eq_rhs expr)
|
177
|
* Printers.pp_node_eq eq))
|
178
|
* defs; *)
|
179
|
if opt then
|
180
|
let new_aliases =
|
181
|
List.map2
|
182
|
(mk_fresh_var
|
183
|
(norm_ctx.parentid, norm_ctx.vars @ vars)
|
184
|
expr.expr_loc)
|
185
|
(Types.type_list_of_type expr.expr_type)
|
186
|
(Clocks.clock_list_of_clock expr.expr_clock)
|
187
|
in
|
188
|
let new_def =
|
189
|
mkeq expr.expr_loc (List.map (fun v -> v.var_id) new_aliases, expr)
|
190
|
in
|
191
|
(* Typing and Registering machine type *)
|
192
|
let _ =
|
193
|
if Machine_types.is_active then
|
194
|
Machine_types.type_def
|
195
|
(norm_ctx.parentid, norm_ctx.vars)
|
196
|
new_aliases expr
|
197
|
in
|
198
|
(new_def :: defs, new_aliases @ vars), replace_expr new_aliases expr
|
199
|
else (defs, vars), expr)
|
200
|
|
201
|
(* Similar fonctions for dimensions *)
|
202
|
let mk_dim_alias opt norm_ctx (defs, vars) dim =
|
203
|
match dim.Dimension.dim_desc with
|
204
|
| Dimension.Dbool _ | Dint _ | Dident _ ->
|
205
|
(defs, vars), dim (* Keep the same *)
|
206
|
| _ when opt ->
|
207
|
(* Cast to expression, normalizing *)
|
208
|
let e = expr_of_dimension dim in
|
209
|
let defvars, e = mk_expr_alias_opt true norm_ctx (defs, vars) e in
|
210
|
defvars, dimension_of_expr e
|
211
|
| _ -> (defs, vars), dim
|
212
|
(* Keep the same *)
|
213
|
|
214
|
let unfold_offsets norm_ctx defvars e offsets =
|
215
|
let add_offset (defvars, e) d =
|
216
|
(*Format.eprintf "add_offset %a(%a) %a @." Printers.pp_expr e Types.pp e.expr_type Dimension.pp_dimension d; *)
|
217
|
let defvars, d =
|
218
|
mk_dim_alias !params.force_alias_internal_fun norm_ctx defvars d
|
219
|
in
|
220
|
let new_e =
|
221
|
{
|
222
|
e with
|
223
|
expr_tag = Utils.new_tag ();
|
224
|
expr_loc = d.Dimension.dim_loc;
|
225
|
expr_type = Types.array_element_type e.expr_type;
|
226
|
expr_desc = Expr_access (e, d);
|
227
|
}
|
228
|
in
|
229
|
defvars, new_e
|
230
|
(*in (Format.eprintf "= %a @." Printers.pp_expr res; res) *)
|
231
|
in
|
232
|
List.fold_left add_offset (defvars, e) offsets
|
233
|
|
234
|
(* Create a (normalized) expression from [ref_e],
|
235
|
replacing description with [norm_d],
|
236
|
taking propagated [offsets] into account
|
237
|
in order to change expression type *)
|
238
|
let mk_norm_expr offsets ref_e norm_d =
|
239
|
(*Format.eprintf "mk_norm_expr %a %a @." Printers.pp_expr ref_e Printers.pp_expr { ref_e with expr_desc = norm_d};*)
|
240
|
let drop_array_type ty = Types.map_tuple_type Types.array_element_type ty in
|
241
|
{
|
242
|
ref_e with
|
243
|
expr_desc = norm_d;
|
244
|
expr_type =
|
245
|
Utils.repeat (List.length offsets) drop_array_type ref_e.expr_type;
|
246
|
}
|
247
|
|
248
|
(* normalize_<foo> : defs * used vars -> <foo> -> (updated defs * updated vars) * normalized <foo> *)
|
249
|
let normalize_list alias norm_ctx offsets norm_element defvars elist =
|
250
|
List.fold_right
|
251
|
(fun t (defvars, qlist) ->
|
252
|
let defvars, norm_t = norm_element alias norm_ctx offsets defvars t in
|
253
|
defvars, norm_t :: qlist)
|
254
|
elist (defvars, [])
|
255
|
|
256
|
let rec normalize_expr ?(alias = true) ?(alias_basic = false) norm_ctx offsets
|
257
|
defvars expr =
|
258
|
(* Format.eprintf "normalize %B %a:%a [%a]@." alias Printers.pp_expr expr Types.pp expr.expr_type (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets; *)
|
259
|
match expr.expr_desc with
|
260
|
| Expr_const _ | Expr_ident _ -> unfold_offsets norm_ctx defvars expr offsets
|
261
|
| Expr_array elist ->
|
262
|
let defvars, norm_elist =
|
263
|
normalize_list alias norm_ctx offsets
|
264
|
(fun _ -> normalize_array_expr ~alias:true)
|
265
|
defvars elist
|
266
|
in
|
267
|
let norm_expr = mk_norm_expr offsets expr (Expr_array norm_elist) in
|
268
|
mk_expr_alias_opt alias norm_ctx defvars norm_expr
|
269
|
| Expr_power (e1, d) when offsets = [] ->
|
270
|
let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in
|
271
|
let norm_expr = mk_norm_expr offsets expr (Expr_power (norm_e1, d)) in
|
272
|
mk_expr_alias_opt alias norm_ctx defvars norm_expr
|
273
|
| Expr_power (e1, _) ->
|
274
|
normalize_expr ~alias norm_ctx (List.tl offsets) defvars e1
|
275
|
| Expr_access (e1, d) ->
|
276
|
normalize_expr ~alias norm_ctx (d :: offsets) defvars e1
|
277
|
| Expr_tuple elist ->
|
278
|
let defvars, norm_elist =
|
279
|
normalize_list alias norm_ctx offsets
|
280
|
(fun alias -> normalize_expr ~alias ~alias_basic:false)
|
281
|
defvars elist
|
282
|
in
|
283
|
defvars, mk_norm_expr offsets expr (Expr_tuple norm_elist)
|
284
|
| Expr_appl (id, args, None)
|
285
|
when Basic_library.is_homomorphic_fun id
|
286
|
&& Types.is_array_type expr.expr_type ->
|
287
|
let defvars, norm_args =
|
288
|
normalize_list alias norm_ctx offsets
|
289
|
(fun _ -> normalize_array_expr ~alias:true)
|
290
|
defvars (expr_list_of_expr args)
|
291
|
in
|
292
|
( defvars,
|
293
|
mk_norm_expr offsets expr
|
294
|
(Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None)) )
|
295
|
| Expr_appl (id, args, None)
|
296
|
when Basic_library.is_expr_internal_fun expr
|
297
|
&& not (!params.force_alias_internal_fun || alias_basic) ->
|
298
|
let defvars, norm_args =
|
299
|
normalize_expr ~alias:true norm_ctx offsets defvars args
|
300
|
in
|
301
|
defvars, mk_norm_expr offsets expr (Expr_appl (id, norm_args, None))
|
302
|
| Expr_appl (id, args, r) ->
|
303
|
let defvars, r =
|
304
|
match r with
|
305
|
| None -> defvars, None
|
306
|
| Some r ->
|
307
|
let defvars, norm_r =
|
308
|
normalize_expr ~alias_basic:true norm_ctx [] defvars r
|
309
|
in
|
310
|
defvars, Some norm_r
|
311
|
in
|
312
|
let defvars, norm_args = normalize_expr norm_ctx [] defvars args in
|
313
|
let norm_expr = mk_norm_expr [] expr (Expr_appl (id, norm_args, r)) in
|
314
|
if offsets <> [] then
|
315
|
let defvars, norm_expr = normalize_expr norm_ctx [] defvars norm_expr in
|
316
|
normalize_expr ~alias norm_ctx offsets defvars norm_expr
|
317
|
else
|
318
|
mk_expr_alias_opt
|
319
|
(alias
|
320
|
&& (!params.force_alias_internal_fun || alias_basic
|
321
|
|| not (Basic_library.is_expr_internal_fun expr)))
|
322
|
norm_ctx defvars norm_expr
|
323
|
| Expr_arrow _ when !params.unfold_arrow_active && not (is_expr_once expr) ->
|
324
|
(* Here we differ from Colaco paper: arrows are pushed to the top *)
|
325
|
normalize_expr ~alias norm_ctx offsets defvars (unfold_arrow expr)
|
326
|
| Expr_arrow (e1, e2) ->
|
327
|
let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in
|
328
|
let defvars, norm_e2 = normalize_expr norm_ctx offsets defvars e2 in
|
329
|
let norm_expr =
|
330
|
mk_norm_expr offsets expr (Expr_arrow (norm_e1, norm_e2))
|
331
|
in
|
332
|
mk_expr_alias_opt alias norm_ctx defvars norm_expr
|
333
|
| Expr_pre e ->
|
334
|
let defvars, norm_e = normalize_expr norm_ctx offsets defvars e in
|
335
|
let norm_expr = mk_norm_expr offsets expr (Expr_pre norm_e) in
|
336
|
mk_expr_alias_opt alias norm_ctx defvars norm_expr
|
337
|
| Expr_fby (e1, e2) ->
|
338
|
let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in
|
339
|
let defvars, norm_e2 = normalize_expr norm_ctx offsets defvars e2 in
|
340
|
let norm_expr = mk_norm_expr offsets expr (Expr_fby (norm_e1, norm_e2)) in
|
341
|
mk_expr_alias_opt alias norm_ctx defvars norm_expr
|
342
|
| Expr_when (e, c, l) ->
|
343
|
let defvars, norm_e = normalize_expr norm_ctx offsets defvars e in
|
344
|
defvars, mk_norm_expr offsets expr (Expr_when (norm_e, c, l))
|
345
|
| Expr_ite (c, t, e) ->
|
346
|
let defvars, norm_c = normalize_guard norm_ctx defvars c in
|
347
|
let defvars, norm_t = normalize_cond_expr norm_ctx offsets defvars t in
|
348
|
let defvars, norm_e = normalize_cond_expr norm_ctx offsets defvars e in
|
349
|
let norm_expr =
|
350
|
mk_norm_expr offsets expr (Expr_ite (norm_c, norm_t, norm_e))
|
351
|
in
|
352
|
mk_expr_alias_opt alias norm_ctx defvars norm_expr
|
353
|
| Expr_merge (c, hl) ->
|
354
|
let defvars, norm_hl = normalize_branches norm_ctx offsets defvars hl in
|
355
|
let norm_expr = mk_norm_expr offsets expr (Expr_merge (c, norm_hl)) in
|
356
|
mk_expr_alias_opt alias norm_ctx defvars norm_expr
|
357
|
|
358
|
(* Creates a conditional with a merge construct, which is more lazy *)
|
359
|
(*
|
360
|
let norm_conditional_as_merge alias node norm_expr offsets defvars expr =
|
361
|
match expr.expr_desc with
|
362
|
| Expr_ite (c, t, e) ->
|
363
|
let defvars, norm_t = norm_expr (alias node offsets defvars t in
|
364
|
| _ -> assert false
|
365
|
*)
|
366
|
and normalize_branches norm_ctx offsets defvars hl =
|
367
|
List.fold_right
|
368
|
(fun (t, h) (defvars, norm_q) ->
|
369
|
let defvars, norm_h = normalize_cond_expr norm_ctx offsets defvars h in
|
370
|
defvars, (t, norm_h) :: norm_q)
|
371
|
hl (defvars, [])
|
372
|
|
373
|
and normalize_array_expr ?(alias = true) norm_ctx offsets defvars expr =
|
374
|
(*Format.eprintf "normalize_array %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*)
|
375
|
match expr.expr_desc with
|
376
|
| Expr_power (e1, d) when offsets = [] ->
|
377
|
let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in
|
378
|
defvars, mk_norm_expr offsets expr (Expr_power (norm_e1, d))
|
379
|
| Expr_power (e1, _) ->
|
380
|
normalize_array_expr ~alias norm_ctx (List.tl offsets) defvars e1
|
381
|
| Expr_access (e1, d) ->
|
382
|
normalize_array_expr ~alias norm_ctx (d :: offsets) defvars e1
|
383
|
| Expr_array elist when offsets = [] ->
|
384
|
let defvars, norm_elist =
|
385
|
normalize_list alias norm_ctx offsets
|
386
|
(fun _ -> normalize_array_expr ~alias:true)
|
387
|
defvars elist
|
388
|
in
|
389
|
defvars, mk_norm_expr offsets expr (Expr_array norm_elist)
|
390
|
| Expr_appl (id, args, None) when Basic_library.is_expr_internal_fun expr ->
|
391
|
let defvars, norm_args =
|
392
|
normalize_list alias norm_ctx offsets
|
393
|
(fun _ -> normalize_array_expr ~alias:true)
|
394
|
defvars (expr_list_of_expr args)
|
395
|
in
|
396
|
( defvars,
|
397
|
mk_norm_expr offsets expr
|
398
|
(Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None)) )
|
399
|
| _ -> normalize_expr ~alias norm_ctx offsets defvars expr
|
400
|
|
401
|
and normalize_cond_expr ?(alias = true) norm_ctx offsets defvars expr =
|
402
|
(* Format.eprintf "normalize_cond %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets; *)
|
403
|
match expr.expr_desc with
|
404
|
| Expr_access (e1, d) ->
|
405
|
normalize_cond_expr ~alias norm_ctx (d :: offsets) defvars e1
|
406
|
| Expr_ite (c, t, e) ->
|
407
|
let defvars, norm_c = normalize_guard norm_ctx defvars c in
|
408
|
let defvars, norm_t = normalize_cond_expr norm_ctx offsets defvars t in
|
409
|
let defvars, norm_e = normalize_cond_expr norm_ctx offsets defvars e in
|
410
|
defvars, mk_norm_expr offsets expr (Expr_ite (norm_c, norm_t, norm_e))
|
411
|
| Expr_merge (c, hl) ->
|
412
|
let defvars, norm_hl = normalize_branches norm_ctx offsets defvars hl in
|
413
|
defvars, mk_norm_expr offsets expr (Expr_merge (c, norm_hl))
|
414
|
| _ when !params.force_alias_ite ->
|
415
|
(* Forcing alias creation for then/else expressions *)
|
416
|
let defvars, norm_expr =
|
417
|
normalize_expr ~alias norm_ctx offsets defvars expr
|
418
|
in
|
419
|
mk_expr_alias_opt true norm_ctx defvars norm_expr
|
420
|
| _ ->
|
421
|
(* default case without the force_alias_ite option *)
|
422
|
normalize_expr ~alias norm_ctx offsets defvars expr
|
423
|
|
424
|
and normalize_guard norm_ctx defvars expr =
|
425
|
let defvars, norm_expr =
|
426
|
normalize_expr ~alias_basic:true norm_ctx [] defvars expr
|
427
|
in
|
428
|
mk_expr_alias_opt true norm_ctx defvars norm_expr
|
429
|
|
430
|
(* outputs cannot be memories as well. If so, introduce new local variable.
|
431
|
*)
|
432
|
let decouple_outputs norm_ctx defvars eq =
|
433
|
let rec fold_lhs defvars lhs tys cks =
|
434
|
match lhs, tys, cks with
|
435
|
| [], [], [] -> defvars, []
|
436
|
| v :: qv, t :: qt, c :: qc ->
|
437
|
let (defs_q, vars_q), lhs_q = fold_lhs defvars qv qt qc in
|
438
|
if norm_ctx.is_output v then
|
439
|
let newvar =
|
440
|
mk_fresh_var (norm_ctx.parentid, norm_ctx.vars) eq.eq_loc t c
|
441
|
in
|
442
|
let neweq = mkeq eq.eq_loc ([ v ], expr_of_vdecl newvar) in
|
443
|
(neweq :: defs_q, newvar :: vars_q), newvar.var_id :: lhs_q
|
444
|
else (defs_q, vars_q), v :: lhs_q
|
445
|
| _ -> assert false
|
446
|
in
|
447
|
let defvars', lhs' =
|
448
|
fold_lhs defvars eq.eq_lhs
|
449
|
(Types.type_list_of_type eq.eq_rhs.expr_type)
|
450
|
(Clocks.clock_list_of_clock eq.eq_rhs.expr_clock)
|
451
|
in
|
452
|
defvars', { eq with eq_lhs = lhs' }
|
453
|
|
454
|
let normalize_eq norm_ctx defvars eq =
|
455
|
(*Format.eprintf "normalize_eq %a@." Types.pp eq.eq_rhs.expr_type;*)
|
456
|
match eq.eq_rhs.expr_desc with
|
457
|
| Expr_pre _ | Expr_fby _ ->
|
458
|
let defvars', eq' = decouple_outputs norm_ctx defvars eq in
|
459
|
let (defs', vars'), norm_rhs =
|
460
|
normalize_expr ~alias:false norm_ctx [] defvars' eq'.eq_rhs
|
461
|
in
|
462
|
let norm_eq = { eq' with eq_rhs = norm_rhs } in
|
463
|
norm_eq :: defs', vars'
|
464
|
| Expr_array _ ->
|
465
|
let (defs', vars'), norm_rhs =
|
466
|
normalize_array_expr ~alias:false norm_ctx [] defvars eq.eq_rhs
|
467
|
in
|
468
|
let norm_eq = { eq with eq_rhs = norm_rhs } in
|
469
|
norm_eq :: defs', vars'
|
470
|
| Expr_appl (id, _, None)
|
471
|
when Basic_library.is_homomorphic_fun id
|
472
|
&& Types.is_array_type eq.eq_rhs.expr_type ->
|
473
|
let (defs', vars'), norm_rhs =
|
474
|
normalize_array_expr ~alias:false norm_ctx [] defvars eq.eq_rhs
|
475
|
in
|
476
|
let norm_eq = { eq with eq_rhs = norm_rhs } in
|
477
|
norm_eq :: defs', vars'
|
478
|
| Expr_appl _ ->
|
479
|
let (defs', vars'), norm_rhs =
|
480
|
normalize_expr ~alias:false norm_ctx [] defvars eq.eq_rhs
|
481
|
in
|
482
|
let norm_eq = { eq with eq_rhs = norm_rhs } in
|
483
|
norm_eq :: defs', vars'
|
484
|
| _ ->
|
485
|
let (defs', vars'), norm_rhs =
|
486
|
normalize_cond_expr ~alias:false norm_ctx [] defvars eq.eq_rhs
|
487
|
in
|
488
|
let norm_eq = { eq with eq_rhs = norm_rhs } in
|
489
|
norm_eq :: defs', vars'
|
490
|
|
491
|
let normalize_eq_split norm_ctx defvars eq =
|
492
|
try
|
493
|
let defs, vars = normalize_eq norm_ctx defvars eq in
|
494
|
List.fold_right
|
495
|
(fun eq (def, vars) ->
|
496
|
let eq_defs = Splitting.tuple_split_eq eq in
|
497
|
if eq_defs = [ eq ] then eq :: def, vars
|
498
|
else List.fold_left (normalize_eq norm_ctx) (def, vars) eq_defs)
|
499
|
defs ([], vars)
|
500
|
with ex ->
|
501
|
Format.eprintf "Issue normalizing eq split: %a@." Printers.pp_node_eq eq;
|
502
|
raise ex
|
503
|
|
504
|
(* Projecting an eexpr to an eexpr associated to a single
|
505
|
variable. Returns the updated ee, the bounded variable and the
|
506
|
associated statement *)
|
507
|
let normalize_pred_eexpr norm_ctx (def, vars) ee =
|
508
|
assert (ee.eexpr_quantifiers = []);
|
509
|
(* We do not normalize quantifiers yet. This is for very far future. *)
|
510
|
(* (\* don't do anything if eexpr is just a variable *\)
|
511
|
* let skip =
|
512
|
* match ee.eexpr_qfexpr.expr_desc with
|
513
|
* | Expr_ident _ | Expr_const _ -> true
|
514
|
* | _ -> false
|
515
|
* in
|
516
|
* if skip then None, ee, (def, vars)
|
517
|
* else *)
|
518
|
(* New output variable *)
|
519
|
let output_id = "spec" ^ string_of_int ee.eexpr_tag in
|
520
|
let output_var =
|
521
|
mkvar_decl ~var_is_contract:true ee.eexpr_loc
|
522
|
( output_id,
|
523
|
mktyp ee.eexpr_loc Tydec_bool,
|
524
|
(* It is a predicate, hence a bool *)
|
525
|
mkclock ee.eexpr_loc Ckdec_any,
|
526
|
false (* not a constant *),
|
527
|
None,
|
528
|
None )
|
529
|
in
|
530
|
(* It is a predicate, hence a bool *)
|
531
|
output_var.var_type <- Type_predef.type_bool;
|
532
|
let output_expr = expr_of_vdecl output_var in
|
533
|
(* Rebuilding an eexpr with a silly expression, just a variable *)
|
534
|
let ee' = { ee with eexpr_qfexpr = output_expr } in
|
535
|
|
536
|
(* Now processing a fresh equation output_id = eexpr_qfexpr. We
|
537
|
inline possible calls within, normalize it and type/clock the
|
538
|
result. *)
|
539
|
let eq = mkeq ee.eexpr_loc ([ output_id ], ee.eexpr_qfexpr) in
|
540
|
|
541
|
(* (\* Inlining any calls *\)
|
542
|
* let nodes = get_nodes decls in
|
543
|
* let calls = ISet.elements (get_expr_calls nodes ee.eexpr_qfexpr) in
|
544
|
* let vars, eqs =
|
545
|
* if calls = [] && not (eq_has_arrows eq) then
|
546
|
* vars, [eq]
|
547
|
* else
|
548
|
* assert false (\* TODO *\)
|
549
|
* in *)
|
550
|
|
551
|
(* Normalizing expr and eqs *)
|
552
|
let defs, vars =
|
553
|
List.fold_left (normalize_eq_split norm_ctx) (def, vars) [ eq ]
|
554
|
in
|
555
|
(* let vars = output_var :: vars in *)
|
556
|
|
557
|
(* let todefine =
|
558
|
List.fold_left
|
559
|
(fun m x-> if List.exists (fun y-> x.var_id = y.var_id) (locals) then m else ISet.add x.var_id m)
|
560
|
(ISet.add output_id ISet.empty) vars in
|
561
|
*)
|
562
|
|
563
|
(* Typing / Clocking *)
|
564
|
try
|
565
|
ignore (Typing.type_var_decl_list vars !Global.type_env vars);
|
566
|
|
567
|
(*
|
568
|
let env = Typing.type_var_decl [] !Global.type_env xxxx output_var in (* typing the variable *)
|
569
|
(* Format.eprintf "typing var %s: %a@." output_id Types.pp output_var.var_type; *)
|
570
|
let env = Typing.type_var_decl_list (vars@node.node_outputs@node.node_inputs) env (vars@node.node_outputs@node.node_inputs) in
|
571
|
(*Format.eprintf "Env: %a@.@?" (Env.pp_env Types.pp) env;*)
|
572
|
let undefined_vars = List.fold_left (Typing.type_eq (env, quant_vars@vars) false) todefine defs in
|
573
|
(* check that table is empty *)
|
574
|
if (not (ISet.is_empty undefined_vars)) then
|
575
|
raise (Types.Error (ee.eexpr_loc, Types.Undefined_var undefined_vars));
|
576
|
|
577
|
(*Format.eprintf "normalized eqs %a@.@?"
|
578
|
(Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs; *)
|
579
|
*)
|
580
|
output_var, ee', (defs, vars)
|
581
|
with Types.Error (loc, err) as exc ->
|
582
|
eprintf "Typing error for eexpr %a: %a%a%a@." Printers.pp_eexpr ee
|
583
|
Types.pp_error err
|
584
|
(pp_comma_list Printers.pp_node_eq)
|
585
|
defs Location.pp loc;
|
586
|
|
587
|
raise exc
|
588
|
|
589
|
(*
|
590
|
|
591
|
let quant_vars = List.flatten (List.map snd ee.eexpr_quantifiers) in
|
592
|
(* Calls are first inlined *)
|
593
|
|
594
|
(*Format.eprintf "eexpr %a@.calls: %a@.@?" Printers.pp_eexpr ee (Utils.fprintf_list ~sep:", " (fun fmt nd -> pp_print_string fmt nd.node_id)) calls; *)
|
595
|
let (new_locals, eqs) =
|
596
|
if calls = [] && not (eq_has_arrows eq) then
|
597
|
(locals, [eq])
|
598
|
else ( (* TODO remettre le code. Je l'ai enleve pour des dependances cycliques *)
|
599
|
(* let new_locals, eqs, asserts = Inliner.inline_eq ~arrows:true eq locals calls in
|
600
|
(*Format.eprintf "eqs %a@.@?"
|
601
|
(Utils.fprintf_list ~sep:", " Printers.pp_node_eq) eqs; *)
|
602
|
(new_locals, eqs)
|
603
|
*)
|
604
|
(locals, [eq])
|
605
|
|
606
|
) in
|
607
|
(* Normalizing expr and eqs *)
|
608
|
let defs, vars = List.fold_left (normalize_eq_split node) ([], new_locals) eqs in
|
609
|
let todefine = List.fold_left
|
610
|
(fun m x-> if List.exists (fun y-> x.var_id = y.var_id) (locals) then m else ISet.add x.var_id m)
|
611
|
(ISet.add output_id ISet.empty) vars in
|
612
|
|
613
|
try
|
614
|
let env = Typing.type_var_decl_list quant_vars !Global.type_env quant_vars in
|
615
|
let env = Typing.type_var_decl [] env output_var in (* typing the variable *)
|
616
|
(* Format.eprintf "typing var %s: %a@." output_id Types.pp output_var.var_type; *)
|
617
|
let env = Typing.type_var_decl_list (vars@node.node_outputs@node.node_inputs) env (vars@node.node_outputs@node.node_inputs) in
|
618
|
(*Format.eprintf "Env: %a@.@?" (Env.pp_env Types.pp) env;*)
|
619
|
let undefined_vars = List.fold_left (Typing.type_eq (env, quant_vars@vars) false) todefine defs in
|
620
|
(* check that table is empty *)
|
621
|
if (not (ISet.is_empty undefined_vars)) then
|
622
|
raise (Types.Error (ee.eexpr_loc, Types.Undefined_var undefined_vars));
|
623
|
|
624
|
(*Format.eprintf "normalized eqs %a@.@?"
|
625
|
(Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs; *)
|
626
|
ee.eexpr_normalized <- Some (output_var, defs, vars)
|
627
|
|
628
|
with (Types.Error (loc,err)) as exc ->
|
629
|
eprintf "Typing error for eexpr %a: %a%a%a@."
|
630
|
Printers.pp_eexpr ee
|
631
|
Types.pp_error err
|
632
|
(Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs
|
633
|
Location.pp_loc loc
|
634
|
|
635
|
|
636
|
;
|
637
|
raise exc
|
638
|
*)
|
639
|
|
640
|
(* We use node local vars to make sure we are creating fresh variables *)
|
641
|
let normalize_spec parentid (in_vars, out_vars, l_vars) s =
|
642
|
(* Original set of variables actually visible from here: in/out and
|
643
|
spec locals (no node locals) *)
|
644
|
let orig_vars = in_vars @ out_vars @ s.locals in
|
645
|
(* Format.eprintf "NormSpec: init locals: %a@." Printers.pp_vars s.locals; *)
|
646
|
let not_is_orig_var v = List.for_all (( != ) v) orig_vars in
|
647
|
let norm_ctx =
|
648
|
{
|
649
|
parentid;
|
650
|
vars = in_vars @ out_vars @ l_vars;
|
651
|
is_output =
|
652
|
(fun _ -> false) (* no need to introduce fresh variables for outputs *);
|
653
|
}
|
654
|
in
|
655
|
(* Normalizing existing stmts *)
|
656
|
let eqs, auts =
|
657
|
List.fold_right
|
658
|
(fun s (el, al) ->
|
659
|
match s with Eq e -> e :: el, al | Aut a -> el, a :: al)
|
660
|
s.stmts ([], [])
|
661
|
in
|
662
|
if auts != [] then assert false;
|
663
|
(* Automata should be expanded by now. *)
|
664
|
let defsvars = List.fold_left (normalize_eq norm_ctx) ([], orig_vars) eqs in
|
665
|
(* Iterate through predicates and normalize them on the go, creating
|
666
|
fresh variables for any guarantees/assumes/require/ensure *)
|
667
|
let process_predicates l defvars =
|
668
|
(* Format.eprintf "ProcPred: vars: %a@." Printers.pp_vars (snd defvars); *)
|
669
|
let res =
|
670
|
List.fold_right
|
671
|
(fun ee (outputs, accu, defvars) ->
|
672
|
let x, ee', defvars = normalize_pred_eexpr norm_ctx defvars ee in
|
673
|
x :: outputs, ee' :: accu, defvars)
|
674
|
l ([], [], defvars)
|
675
|
in
|
676
|
(* Format.eprintf "ProcStmt: %a@." Printers.pp_node_eqs (fst (snd res));
|
677
|
* Format.eprintf "ProcPred: vars: %a@." Printers.pp_vars (snd (snd res)); *)
|
678
|
res
|
679
|
in
|
680
|
|
681
|
let outs_asm, assume', defsvars = process_predicates s.assume defsvars in
|
682
|
let outs_grt, guarantees', defsvars = process_predicates s.guarantees defsvars in
|
683
|
let outs, modes', (defs, vars) =
|
684
|
List.fold_right
|
685
|
(fun m (outs, accu_m, defsvars) ->
|
686
|
let outs_req, require', defsvars = process_predicates m.require defsvars in
|
687
|
let outs_ens, ensure', defsvars = process_predicates m.ensure defsvars in
|
688
|
outs_req @ outs_ens @ outs,
|
689
|
{ m with require = require'; ensure = ensure' } :: accu_m,
|
690
|
defsvars)
|
691
|
s.modes (outs_asm @ outs_grt, [], defsvars)
|
692
|
in
|
693
|
|
694
|
let new_locals = List.filter not_is_orig_var vars in
|
695
|
(* removing inouts and initial locals ones *)
|
696
|
( new_locals,
|
697
|
outs,
|
698
|
defs,
|
699
|
{
|
700
|
s with
|
701
|
(* locals = s.locals @ new_locals; *)
|
702
|
stmts = [];
|
703
|
assume = assume';
|
704
|
guarantees = guarantees';
|
705
|
modes = modes';
|
706
|
} )
|
707
|
(* let nee _ = () in
|
708
|
* (\*normalize_eexpr decls iovars in *\)
|
709
|
* List.iter nee s.assume;
|
710
|
* List.iter nee s.guarantees;
|
711
|
* List.iter (fun m ->
|
712
|
* List.iter nee m.require;
|
713
|
* List.iter nee m.ensure
|
714
|
* ) s.modes; *)
|
715
|
|
716
|
(* The normalization phase introduces new local variables
|
717
|
- output cannot be memories. If this happen, new local variables acting as
|
718
|
memories are introduced.
|
719
|
- array constants, pre, arrow, fby, ite, merge, calls to node with index
|
720
|
access
|
721
|
Thoses values are shared, ie. no duplicate expressions are introduced.
|
722
|
|
723
|
Concerning specification, a similar process is applied, replacing an
|
724
|
expression by a list of local variables and definitions
|
725
|
*)
|
726
|
|
727
|
(** normalize_node node returns a normalized node,
|
728
|
ie.
|
729
|
- updated locals
|
730
|
- new equations
|
731
|
-
|
732
|
*)
|
733
|
let normalize_node ?(first=true) node =
|
734
|
reset_cpt_fresh ();
|
735
|
let orig_vars = node.node_inputs @ node.node_outputs @ node.node_locals in
|
736
|
let not_is_orig_var v = List.for_all (( != ) v) orig_vars in
|
737
|
let norm_ctx =
|
738
|
{
|
739
|
parentid = node.node_id;
|
740
|
vars = get_node_vars node;
|
741
|
is_output =
|
742
|
(fun vid -> List.exists (fun v -> v.var_id = vid) node.node_outputs);
|
743
|
}
|
744
|
in
|
745
|
|
746
|
let eqs, auts = get_node_eqs node in
|
747
|
if auts != [] then assert false;
|
748
|
(* Automata should be expanded by now. *)
|
749
|
let node_spec, new_vars, new_outs, eqs =
|
750
|
(* Update mutable fields of eexpr to perform normalization of
|
751
|
specification.
|
752
|
|
753
|
Careful: we do not normalize annotations, since they can have the form
|
754
|
x = (a, b, c) *)
|
755
|
match node.node_spec with
|
756
|
| None | Some (NodeSpec _) ->
|
757
|
node.node_spec, [], [], eqs
|
758
|
| Some (Contract s) ->
|
759
|
let new_locals, new_outs, new_stmts, s' =
|
760
|
normalize_spec node.node_id
|
761
|
(node.node_inputs, node.node_outputs, node.node_locals)
|
762
|
s
|
763
|
in
|
764
|
(* Format.eprintf "Normalization bounded new locals: %a@." Printers.pp_vars new_locals;
|
765
|
* Format.eprintf "Normalization bounded stmts: %a@." Printers.pp_node_eqs new_stmts; *)
|
766
|
Some (Contract s'), new_locals, new_outs, new_stmts @ eqs
|
767
|
in
|
768
|
let defs, vars =
|
769
|
List.fold_left (normalize_eq norm_ctx) ([], new_vars @ orig_vars) eqs
|
770
|
in
|
771
|
(* Normalize the asserts *)
|
772
|
let vars, assert_defs, node_asserts =
|
773
|
List.fold_left
|
774
|
(fun (vars, def_accu, assert_accu) assert_ ->
|
775
|
let assert_expr = assert_.assert_expr in
|
776
|
let (defs, vars'), expr =
|
777
|
normalize_expr ~alias:true
|
778
|
(* forcing introduction of new equations for fcn calls *)
|
779
|
norm_ctx []
|
780
|
(* empty offset for arrays *)
|
781
|
([], vars)
|
782
|
(* defvar only contains vars *)
|
783
|
assert_expr
|
784
|
in
|
785
|
(*Format.eprintf "New assert vars: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) vars';*)
|
786
|
( vars',
|
787
|
defs @ def_accu,
|
788
|
{ assert_ with assert_expr = expr } :: assert_accu ))
|
789
|
(vars, [], []) node.node_asserts
|
790
|
in
|
791
|
let new_locals = List.filter not_is_orig_var vars in
|
792
|
|
793
|
(* we filter out inout
|
794
|
vars and initial locals ones *)
|
795
|
let node_locals = node.node_locals @ new_locals in
|
796
|
|
797
|
(* we add again, at the
|
798
|
beginning of the list the
|
799
|
local declared ones *)
|
800
|
(*Format.eprintf "New locals: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) new_locals;*)
|
801
|
|
802
|
(* Updating annotations: traceability and machine types for fresh variables *)
|
803
|
|
804
|
(* Compute traceability info:
|
805
|
- gather newly bound variables
|
806
|
- compute the associated expression without aliases
|
807
|
*)
|
808
|
let new_annots =
|
809
|
if !Options.traces then
|
810
|
let diff_vars =
|
811
|
List.filter (fun v -> not (List.mem v node.node_locals)) node_locals
|
812
|
in
|
813
|
let norm_traceability =
|
814
|
{
|
815
|
annots =
|
816
|
List.map
|
817
|
(fun v ->
|
818
|
let eq =
|
819
|
try
|
820
|
List.find
|
821
|
(fun eq ->
|
822
|
List.exists (fun v' -> v' = v.var_id) eq.eq_lhs)
|
823
|
(defs @ assert_defs)
|
824
|
with Not_found ->
|
825
|
Format.eprintf
|
826
|
"Traceability annotation generation: var %s not found@."
|
827
|
v.var_id;
|
828
|
assert false
|
829
|
in
|
830
|
let expr =
|
831
|
substitute_expr diff_vars (defs @ assert_defs) eq.eq_rhs
|
832
|
in
|
833
|
let pair =
|
834
|
mkeexpr expr.expr_loc
|
835
|
(mkexpr expr.expr_loc
|
836
|
(Expr_tuple
|
837
|
[ expr_of_ident v.var_id expr.expr_loc; expr ]))
|
838
|
in
|
839
|
Annotations.add_expr_ann node.node_id pair.eexpr_tag
|
840
|
[ "traceability" ];
|
841
|
[ "traceability" ], pair)
|
842
|
diff_vars;
|
843
|
annot_loc = Location.dummy;
|
844
|
}
|
845
|
in
|
846
|
norm_traceability :: node.node_annot
|
847
|
else node.node_annot
|
848
|
in
|
849
|
|
850
|
let node_annot =
|
851
|
List.fold_left
|
852
|
(fun annots v ->
|
853
|
if Machine_types.is_active && Machine_types.is_exportable v then (
|
854
|
let typ = Machine_types.get_specified_type v in
|
855
|
let typ_name = Machine_types.type_name typ in
|
856
|
|
857
|
let loc = v.var_loc in
|
858
|
let typ_as_string = mkexpr loc (Expr_const (Const_string typ_name)) in
|
859
|
let pair =
|
860
|
expr_to_eexpr
|
861
|
(expr_of_expr_list loc [ expr_of_vdecl v; typ_as_string ])
|
862
|
in
|
863
|
Annotations.add_expr_ann node.node_id pair.eexpr_tag
|
864
|
Machine_types.keywords;
|
865
|
{ annots = [ Machine_types.keywords, pair ]; annot_loc = loc }
|
866
|
:: annots)
|
867
|
else annots)
|
868
|
new_annots new_locals
|
869
|
in
|
870
|
|
871
|
let node_inputs, node_outputs =
|
872
|
if node.node_iscontract && first then
|
873
|
node.node_inputs @ node.node_outputs, new_outs
|
874
|
else
|
875
|
node.node_inputs, node.node_outputs
|
876
|
in
|
877
|
|
878
|
let node =
|
879
|
{
|
880
|
node with
|
881
|
node_inputs;
|
882
|
node_outputs;
|
883
|
node_locals;
|
884
|
node_stmts = List.map (fun eq -> Eq eq) (defs @ assert_defs);
|
885
|
node_asserts;
|
886
|
node_annot;
|
887
|
node_spec
|
888
|
}
|
889
|
in
|
890
|
(*Printers.pp_node Format.err_formatter node;*)
|
891
|
node
|
892
|
|
893
|
let normalize_inode nd =
|
894
|
reset_cpt_fresh ();
|
895
|
match nd.nodei_spec with
|
896
|
| None | Some (NodeSpec _) -> nd
|
897
|
| Some (Contract _) -> assert false
|
898
|
|
899
|
let normalize_decl ?first (decl : top_decl) : top_decl =
|
900
|
match decl.top_decl_desc with
|
901
|
| Node nd ->
|
902
|
let decl' = { decl with top_decl_desc = Node (normalize_node ?first nd) } in
|
903
|
update_node nd.node_id decl';
|
904
|
decl'
|
905
|
| ImportedNode nd ->
|
906
|
let decl' =
|
907
|
{ decl with top_decl_desc = ImportedNode (normalize_inode nd) }
|
908
|
in
|
909
|
update_node nd.nodei_id decl';
|
910
|
decl'
|
911
|
| Include _ | Open _ | Const _ | TypeDef _ -> decl
|
912
|
|
913
|
let normalize_prog ?first p decls =
|
914
|
(* Backend specific configurations for normalization *)
|
915
|
params := p;
|
916
|
|
917
|
(* Main algorithm: iterates over nodes *)
|
918
|
List.map (normalize_decl ?first) decls
|
919
|
|
920
|
(* Fake interface for outside uses *)
|
921
|
let mk_expr_alias_opt opt (parentid, ctx_vars) (defs, vars) expr =
|
922
|
mk_expr_alias_opt opt
|
923
|
{ parentid; vars = ctx_vars; is_output = (fun _ -> false) }
|
924
|
(defs, vars) expr
|
925
|
|
926
|
(* Local Variables: *)
|
927
|
(* compile-command:"make -C .." *)
|
928
|
(* End: *)
|