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 Lustre_types
|
13
|
open Machine_code_types
|
14
|
open Machine_code_common
|
15
|
open Spec_types
|
16
|
open Spec_common
|
17
|
open Corelang
|
18
|
open Clocks
|
19
|
open Causality
|
20
|
open Utils
|
21
|
|
22
|
exception NormalizationError
|
23
|
|
24
|
(* Questions:
|
25
|
|
26
|
- where are used the mconst. They contain initialization of constant in
|
27
|
nodes. But they do not seem to be used by c_backend *)
|
28
|
|
29
|
(* translate_<foo> : vars -> context -> <foo> -> machine code/expression *)
|
30
|
(* the context contains m : state aka memory variables *)
|
31
|
(* si : initialization instructions *)
|
32
|
(* j : node aka machine instances *)
|
33
|
(* d : local variables *)
|
34
|
(* s : step instructions *)
|
35
|
|
36
|
(* Machine processing requires knowledge about variables and local variables.
|
37
|
Local could be memories while other could not. *)
|
38
|
type machine_env = { is_local : string -> bool; get_var : string -> var_decl }
|
39
|
|
40
|
let build_env inputs locals outputs =
|
41
|
let all = List.sort_uniq VDeclModule.compare (locals @ inputs @ outputs) in
|
42
|
{
|
43
|
is_local = (fun id -> List.exists (fun v -> v.var_id = id) locals);
|
44
|
get_var =
|
45
|
(fun id ->
|
46
|
try List.find (fun v -> v.var_id = id) all
|
47
|
with Not_found ->
|
48
|
(* Format.eprintf "Impossible to find variable %s in set %a@.@?" * id
|
49
|
* VSet.pp all; *)
|
50
|
raise Not_found);
|
51
|
}
|
52
|
|
53
|
(****************************************************************)
|
54
|
(* Basic functions to translate to machine values, instructions *)
|
55
|
(****************************************************************)
|
56
|
|
57
|
let translate_ident env id =
|
58
|
(* Format.eprintf "trnaslating ident: %s@." id; *)
|
59
|
(* id is a var that shall be visible here , ie. in vars *)
|
60
|
try
|
61
|
let var_id = env.get_var id in
|
62
|
vdecl_to_val var_id
|
63
|
with Not_found -> (
|
64
|
(* id is a constant *)
|
65
|
try
|
66
|
let vdecl =
|
67
|
Corelang.var_decl_of_const
|
68
|
(const_of_top (Hashtbl.find Corelang.consts_table id))
|
69
|
in
|
70
|
vdecl_to_val vdecl
|
71
|
with Not_found -> (
|
72
|
(* id is a tag, getting its type in the list of declared enums *)
|
73
|
try id_to_tag id
|
74
|
with Not_found ->
|
75
|
Format.eprintf "internal error: Machine_code.translate_ident %s@.@?" id;
|
76
|
assert false))
|
77
|
|
78
|
(* specialize predefined (polymorphic) operators wrt their instances, so that
|
79
|
the C semantics is preserved *)
|
80
|
let specialize_to_c expr =
|
81
|
match expr.expr_desc with
|
82
|
| Expr_appl (id, e, r) ->
|
83
|
if
|
84
|
List.exists
|
85
|
(fun e -> Types.is_bool_type e.expr_type)
|
86
|
(expr_list_of_expr e)
|
87
|
then
|
88
|
let id = match id with "=" -> "equi" | "!=" -> "xor" | _ -> id in
|
89
|
{ expr with expr_desc = Expr_appl (id, e, r) }
|
90
|
else expr
|
91
|
| _ ->
|
92
|
expr
|
93
|
|
94
|
let specialize_op expr =
|
95
|
match !Options.output with Options.OutC -> specialize_to_c expr | _ -> expr
|
96
|
|
97
|
let rec translate_expr env expr =
|
98
|
let expr = specialize_op expr in
|
99
|
let translate_expr = translate_expr env in
|
100
|
let value_desc =
|
101
|
match expr.expr_desc with
|
102
|
| Expr_const v ->
|
103
|
Cst v
|
104
|
| Expr_ident x ->
|
105
|
(translate_ident env x).value_desc
|
106
|
| Expr_array el ->
|
107
|
Array (List.map translate_expr el)
|
108
|
| Expr_access (t, i) ->
|
109
|
Access (translate_expr t, translate_expr (expr_of_dimension i))
|
110
|
| Expr_power (e, n) ->
|
111
|
Power (translate_expr e, translate_expr (expr_of_dimension n))
|
112
|
| Expr_when (e1, _, _) ->
|
113
|
(translate_expr e1).value_desc
|
114
|
| Expr_appl (id, e, _) when Basic_library.is_expr_internal_fun expr ->
|
115
|
let nd = node_from_name id in
|
116
|
Fun (node_name nd, List.map translate_expr (expr_list_of_expr e))
|
117
|
| Expr_ite (g, t, e) when Backends.is_functional () ->
|
118
|
(* special treatment depending on the active backend. For functional ones,
|
119
|
like horn backend, ite are preserved in expression. While they are
|
120
|
removed for C or Java backends. *)
|
121
|
Fun ("ite", [ translate_expr g; translate_expr t; translate_expr e ])
|
122
|
| _ ->
|
123
|
Format.eprintf
|
124
|
"Normalization error for backend %t: %a@."
|
125
|
Options.pp_output
|
126
|
Printers.pp_expr
|
127
|
expr;
|
128
|
raise NormalizationError
|
129
|
in
|
130
|
mk_val value_desc expr.expr_type
|
131
|
|
132
|
let translate_guard env expr =
|
133
|
match expr.expr_desc with
|
134
|
| Expr_ident x ->
|
135
|
translate_ident env x
|
136
|
| _ ->
|
137
|
Format.eprintf "internal error: translate_guard %a@." Printers.pp_expr expr;
|
138
|
assert false
|
139
|
|
140
|
let rec translate_act env (y, expr) =
|
141
|
let translate_act = translate_act env in
|
142
|
let translate_guard = translate_guard env in
|
143
|
let translate_expr = translate_expr env in
|
144
|
let lustre_eq = Corelang.mkeq Location.dummy ([ y.var_id ], expr) in
|
145
|
match expr.expr_desc with
|
146
|
| Expr_ite (c, t, e) ->
|
147
|
let c = translate_guard c in
|
148
|
let t, spec_t = translate_act (y, t) in
|
149
|
let e, spec_e = translate_act (y, e) in
|
150
|
mk_conditional ~lustre_eq c [ t ] [ e ], mk_conditional_tr c spec_t spec_e
|
151
|
| Expr_merge (x, hl) ->
|
152
|
let var_x = env.get_var x in
|
153
|
let hl, spec_hl =
|
154
|
List.(
|
155
|
split
|
156
|
(map
|
157
|
(fun (t, h) ->
|
158
|
let h, spec_h = translate_act (y, h) in
|
159
|
(t, [ h ]), (t, spec_h))
|
160
|
hl))
|
161
|
in
|
162
|
mk_branch' ~lustre_eq var_x hl, mk_branch_tr var_x spec_hl
|
163
|
| _ ->
|
164
|
let e = translate_expr expr in
|
165
|
mk_assign ~lustre_eq y e, mk_assign_tr y e
|
166
|
|
167
|
let get_memory env mems eq =
|
168
|
match eq.eq_lhs, eq.eq_rhs.expr_desc with
|
169
|
| ([ x ], Expr_pre _ | [ x ], Expr_fby _) when env.is_local x ->
|
170
|
let var_x = env.get_var x in
|
171
|
VSet.add var_x mems
|
172
|
| _ ->
|
173
|
mems
|
174
|
|
175
|
let get_memories env = List.fold_left (get_memory env) VSet.empty
|
176
|
|
177
|
(* Datastructure updated while visiting equations *)
|
178
|
type machine_ctx = {
|
179
|
(* memories *)
|
180
|
m : ISet.t;
|
181
|
(* Reset instructions *)
|
182
|
si : instr_t list;
|
183
|
(* Instances *)
|
184
|
j : (Lustre_types.top_decl * Dimension.t list) IMap.t;
|
185
|
(* Step instructions *)
|
186
|
s : instr_t list;
|
187
|
(* Memory pack spec *)
|
188
|
mp : mc_formula_t list;
|
189
|
(* Transition spec *)
|
190
|
t :
|
191
|
(var_decl list
|
192
|
(* vars *)
|
193
|
* ISet.t (* memory footprint *)
|
194
|
* ident IMap.t
|
195
|
(* memory instances footprint *)
|
196
|
* mc_formula_t)
|
197
|
(* formula *)
|
198
|
list;
|
199
|
}
|
200
|
|
201
|
let ctx_init =
|
202
|
{ m = ISet.empty; si = []; j = IMap.empty; s = []; mp = []; t = [] }
|
203
|
|
204
|
(****************************************************************)
|
205
|
(* Main function to translate equations into this machine context we are
|
206
|
building *)
|
207
|
(****************************************************************)
|
208
|
|
209
|
let mk_control v l inst = mkinstr (MBranch (vdecl_to_val v, [ l, [ inst ] ]))
|
210
|
|
211
|
let control_on_clock env ck inst =
|
212
|
let rec aux ((fspec, inst) as acc) ck =
|
213
|
match (Clocks.repr ck).cdesc with
|
214
|
| Con (ck, cr, l) ->
|
215
|
let id = Clocks.const_of_carrier cr in
|
216
|
let v = env.get_var id in
|
217
|
aux
|
218
|
( (fun spec -> Imply (Equal (Var v, Tag l), fspec spec)),
|
219
|
mk_control v l inst )
|
220
|
ck
|
221
|
| _ ->
|
222
|
acc
|
223
|
in
|
224
|
let fspec, inst = aux ((fun spec -> spec), inst) ck in
|
225
|
fspec, inst
|
226
|
|
227
|
let reset_instance env i r c =
|
228
|
match r with
|
229
|
| Some r ->
|
230
|
let r = translate_guard env r in
|
231
|
let _, inst =
|
232
|
control_on_clock
|
233
|
env
|
234
|
c
|
235
|
(mk_conditional r [ mkinstr (MSetReset i) ] [ mkinstr (MNoReset i) ])
|
236
|
in
|
237
|
Some r, [ inst ]
|
238
|
| None ->
|
239
|
None, []
|
240
|
|
241
|
let translate_eq env ctx nd inputs locals outputs i eq =
|
242
|
let id = nd.node_id in
|
243
|
let translate_expr = translate_expr env in
|
244
|
let translate_act = translate_act env in
|
245
|
let locals_pi = Lustre_live.inter_live_i_with id (i - 1) locals in
|
246
|
let outputs_pi = Lustre_live.inter_live_i_with id (i - 1) outputs in
|
247
|
let locals_i = Lustre_live.inter_live_i_with id i locals in
|
248
|
let outputs_i = Lustre_live.inter_live_i_with id i outputs in
|
249
|
let pred_mp ctx a = And [ mk_memory_pack ~i:(i - 1) id; a ] :: ctx.mp in
|
250
|
let pred_t ctx a =
|
251
|
( inputs @ locals_i @ outputs_i,
|
252
|
ctx.m,
|
253
|
IMap.map (fun (td, _) -> node_name td) ctx.j,
|
254
|
Exists
|
255
|
( Lustre_live.existential_vars id i eq (locals @ outputs),
|
256
|
And
|
257
|
[
|
258
|
mk_transition
|
259
|
~i:(i - 1)
|
260
|
id
|
261
|
(vdecls_to_vals (inputs @ locals_pi @ outputs_pi));
|
262
|
a;
|
263
|
] ) )
|
264
|
:: ctx.t
|
265
|
in
|
266
|
let control_on_clock ck inst spec_mp spec_t ctx =
|
267
|
let fspec, inst = control_on_clock env ck inst in
|
268
|
{
|
269
|
ctx with
|
270
|
s =
|
271
|
{
|
272
|
inst with
|
273
|
instr_spec =
|
274
|
(if fst (get_stateless_status_node nd) then []
|
275
|
else [ mk_memory_pack ~i id ])
|
276
|
@ [
|
277
|
mk_transition
|
278
|
~i
|
279
|
id
|
280
|
(vdecls_to_vals (inputs @ locals_i @ outputs_i));
|
281
|
];
|
282
|
}
|
283
|
:: ctx.s;
|
284
|
mp = pred_mp ctx spec_mp;
|
285
|
t = pred_t ctx (fspec spec_t);
|
286
|
}
|
287
|
in
|
288
|
let reset_instance = reset_instance env in
|
289
|
let mkinstr' = mkinstr ~lustre_eq:eq in
|
290
|
let ctl ?(ck = eq.eq_rhs.expr_clock) instr =
|
291
|
control_on_clock ck (mkinstr' instr)
|
292
|
in
|
293
|
|
294
|
(* Format.eprintf "translate_eq %a with clock %a@." Printers.pp_node_eq eq
|
295
|
Clocks.print_ck eq.eq_rhs.expr_clock; *)
|
296
|
match eq.eq_lhs, eq.eq_rhs.expr_desc with
|
297
|
| [ x ], Expr_arrow (e1, e2) ->
|
298
|
let var_x = env.get_var x in
|
299
|
let td = Arrow.arrow_top_decl () in
|
300
|
let inst = new_instance td eq.eq_rhs.expr_tag in
|
301
|
let c1 = translate_expr e1 in
|
302
|
let c2 = translate_expr e2 in
|
303
|
assert (c1.value_desc = Cst (Const_tag "true"));
|
304
|
assert (c2.value_desc = Cst (Const_tag "false"));
|
305
|
let ctx =
|
306
|
ctl
|
307
|
(MStep ([ var_x ], inst, [ c1; c2 ]))
|
308
|
(mk_memory_pack ~inst (node_name td))
|
309
|
(mk_transition ~inst (node_name td) [ vdecl_to_val var_x ])
|
310
|
{ ctx with j = IMap.add inst (td, []) ctx.j }
|
311
|
in
|
312
|
{ ctx with si = mkinstr (MSetReset inst) :: ctx.si }
|
313
|
| [ x ], Expr_pre e when env.is_local x ->
|
314
|
let var_x = env.get_var x in
|
315
|
let e = translate_expr e in
|
316
|
ctl
|
317
|
(MStateAssign (var_x, e))
|
318
|
(mk_state_variable_pack var_x)
|
319
|
(mk_state_assign_tr var_x e)
|
320
|
{ ctx with m = ISet.add x ctx.m }
|
321
|
| [ x ], Expr_fby (e1, e2) when env.is_local x ->
|
322
|
let var_x = env.get_var x in
|
323
|
let e2 = translate_expr e2 in
|
324
|
let ctx =
|
325
|
ctl
|
326
|
(MStateAssign (var_x, e2))
|
327
|
(mk_state_variable_pack var_x)
|
328
|
(mk_state_assign_tr var_x e2)
|
329
|
{ ctx with m = ISet.add x ctx.m }
|
330
|
in
|
331
|
{
|
332
|
ctx with
|
333
|
si = mkinstr' (MStateAssign (var_x, translate_expr e1)) :: ctx.si;
|
334
|
}
|
335
|
| p, Expr_appl (f, arg, r)
|
336
|
when not (Basic_library.is_expr_internal_fun eq.eq_rhs) ->
|
337
|
let var_p = List.map env.get_var p in
|
338
|
let el = expr_list_of_expr arg in
|
339
|
let vl = List.map translate_expr el in
|
340
|
let node_f = node_from_name f in
|
341
|
let call_f = node_f, NodeDep.filter_static_inputs (node_inputs node_f) el in
|
342
|
let inst = new_instance node_f eq.eq_rhs.expr_tag in
|
343
|
let env_cks =
|
344
|
List.fold_right
|
345
|
(fun arg cks -> arg.expr_clock :: cks)
|
346
|
el
|
347
|
[ eq.eq_rhs.expr_clock ]
|
348
|
in
|
349
|
let call_ck =
|
350
|
Clock_calculus.compute_root_clock (Clock_predef.ck_tuple env_cks)
|
351
|
in
|
352
|
let r, reset_inst = reset_instance inst r call_ck in
|
353
|
let ctx =
|
354
|
ctl
|
355
|
~ck:call_ck
|
356
|
(MStep (var_p, inst, vl))
|
357
|
(mk_memory_pack ~inst (node_name node_f))
|
358
|
(mk_transition ?r ~inst (node_name node_f) (vl @ vdecls_to_vals var_p))
|
359
|
{
|
360
|
ctx with
|
361
|
j = IMap.add inst call_f ctx.j;
|
362
|
s = (if Stateless.check_node node_f then [] else reset_inst) @ ctx.s;
|
363
|
}
|
364
|
in
|
365
|
(*Clocks.new_var true in Clock_calculus.unify_imported_clock (Some call_ck)
|
366
|
eq.eq_rhs.expr_clock eq.eq_rhs.expr_loc; Format.eprintf "call %a: %a:
|
367
|
%a@," Printers.pp_expr eq.eq_rhs Clocks.print_ck (Clock_predef.ck_tuple
|
368
|
env_cks) Clocks.print_ck call_ck;*)
|
369
|
{
|
370
|
ctx with
|
371
|
si =
|
372
|
(if Stateless.check_node node_f then ctx.si
|
373
|
else mkinstr (MSetReset inst) :: ctx.si);
|
374
|
}
|
375
|
| [ x ], _ ->
|
376
|
begin try
|
377
|
let var_x = env.get_var x in
|
378
|
let instr, spec = translate_act (var_x, eq.eq_rhs) in
|
379
|
control_on_clock eq.eq_rhs.expr_clock instr True spec ctx
|
380
|
with Not_found ->
|
381
|
Format.eprintf "ERROR: node %s, eq %a@." id Printers.pp_node_eq eq ;
|
382
|
raise Not_found
|
383
|
end
|
384
|
| _ ->
|
385
|
Format.eprintf
|
386
|
"internal error: Machine_code.translate_eq %a@?"
|
387
|
Printers.pp_node_eq
|
388
|
eq;
|
389
|
assert false
|
390
|
|
391
|
let constant_equations locals =
|
392
|
List.fold_left
|
393
|
(fun eqs vdecl ->
|
394
|
if vdecl.var_dec_const then
|
395
|
{
|
396
|
eq_lhs = [ vdecl.var_id ];
|
397
|
eq_rhs = desome vdecl.var_dec_value;
|
398
|
eq_loc = vdecl.var_loc;
|
399
|
}
|
400
|
:: eqs
|
401
|
else eqs)
|
402
|
[]
|
403
|
locals
|
404
|
|
405
|
let translate_eqs env ctx nd inputs locals outputs eqs =
|
406
|
List.fold_left
|
407
|
(fun (ctx, i) eq ->
|
408
|
let ctx = translate_eq env ctx nd inputs locals outputs i eq in
|
409
|
ctx, i + 1)
|
410
|
(ctx, 1)
|
411
|
eqs
|
412
|
|> fst
|
413
|
|
414
|
(****************************************************************)
|
415
|
(* Processing nodes *)
|
416
|
(****************************************************************)
|
417
|
|
418
|
let process_asserts nd =
|
419
|
let exprl = List.map (fun assert_ -> assert_.assert_expr) nd.node_asserts in
|
420
|
if Backends.is_functional () then [], [], exprl
|
421
|
else
|
422
|
(* Each assert(e) is associated to a fresh variable v and declared as v=e;
|
423
|
assert (v); *)
|
424
|
let _, vars, eql, assertl =
|
425
|
List.fold_left
|
426
|
(fun (i, vars, eqlist, assertlist) expr ->
|
427
|
let loc = expr.expr_loc in
|
428
|
let var_id = nd.node_id ^ "_assert_" ^ string_of_int i in
|
429
|
let assert_var =
|
430
|
mkvar_decl
|
431
|
loc
|
432
|
~orig:false
|
433
|
(* fresh var *)
|
434
|
( var_id,
|
435
|
mktyp loc Tydec_bool,
|
436
|
mkclock loc Ckdec_any,
|
437
|
false,
|
438
|
(* not a constant *)
|
439
|
None,
|
440
|
(* no default value *)
|
441
|
Some nd.node_id )
|
442
|
in
|
443
|
assert_var.var_type <- Type_predef.type_bool
|
444
|
(* Types.new_ty (Types.Tbool) *);
|
445
|
let eq = mkeq loc ([ var_id ], expr) in
|
446
|
( i + 1,
|
447
|
assert_var :: vars,
|
448
|
eq :: eqlist,
|
449
|
{ expr with expr_desc = Expr_ident var_id } :: assertlist ))
|
450
|
(1, [], [], [])
|
451
|
exprl
|
452
|
in
|
453
|
vars, eql, assertl
|
454
|
|
455
|
let translate_core env nd sorted_eqs inputs locals outputs =
|
456
|
let constant_eqs = constant_equations locals in
|
457
|
|
458
|
(* Compute constants' instructions *)
|
459
|
let ctx0 = translate_eqs env ctx_init nd inputs locals outputs constant_eqs in
|
460
|
assert (ctx0.si = []);
|
461
|
assert (IMap.is_empty ctx0.j);
|
462
|
|
463
|
(* Compute ctx for all eqs *)
|
464
|
let ctx = translate_eqs env ctx_init nd inputs locals outputs sorted_eqs in
|
465
|
|
466
|
ctx, ctx0.s
|
467
|
|
468
|
let zero = mk_val (Cst (Const_int 0)) Type_predef.type_int
|
469
|
|
470
|
let memory_pack_0 nd =
|
471
|
{
|
472
|
mpname = nd;
|
473
|
mpindex = Some 0;
|
474
|
mpformula =
|
475
|
And [ StateVarPack ResetFlag; Equal (Memory ResetFlag, Val zero) ];
|
476
|
}
|
477
|
|
478
|
let memory_pack_toplevel nd i =
|
479
|
{
|
480
|
mpname = nd;
|
481
|
mpindex = None;
|
482
|
mpformula =
|
483
|
Ternary
|
484
|
(Memory ResetFlag, StateVarPack ResetFlag, mk_memory_pack ~i nd.node_id);
|
485
|
}
|
486
|
|
487
|
let transition_0 nd =
|
488
|
{
|
489
|
tname = nd;
|
490
|
tindex = Some 0;
|
491
|
tvars = nd.node_inputs;
|
492
|
tformula = if fst (get_stateless_status_node nd) then True else StateVarPack ResetFlag;
|
493
|
tmem_footprint = ISet.empty;
|
494
|
tinst_footprint = IMap.empty;
|
495
|
}
|
496
|
|
497
|
let transition_toplevel nd i =
|
498
|
let tr =
|
499
|
mk_transition
|
500
|
nd.node_id
|
501
|
~i
|
502
|
(vdecls_to_vals (nd.node_inputs @ nd.node_outputs))
|
503
|
in
|
504
|
{
|
505
|
tname = nd;
|
506
|
tindex = None;
|
507
|
tvars = nd.node_inputs @ nd.node_outputs;
|
508
|
tformula =
|
509
|
(if fst (get_stateless_status_node nd) then tr
|
510
|
else ExistsMem (nd.node_id, Predicate (ResetCleared nd.node_id), tr));
|
511
|
tmem_footprint = ISet.empty;
|
512
|
tinst_footprint = IMap.empty;
|
513
|
}
|
514
|
|
515
|
let translate_eexpr env e =
|
516
|
try
|
517
|
List.fold_right (fun (qt, xs) f -> match qt with
|
518
|
| Lustre_types.Exists -> Exists (xs, f)
|
519
|
| Lustre_types.Forall -> Forall (xs, f))
|
520
|
e.eexpr_quantifiers
|
521
|
(Value (translate_expr env e.eexpr_qfexpr))
|
522
|
with
|
523
|
NormalizationError ->
|
524
|
Format.eprintf
|
525
|
"Normalization error: %a@."
|
526
|
Printers.pp_eexpr
|
527
|
e;
|
528
|
raise NormalizationError
|
529
|
|
530
|
|
531
|
let translate_contract env c = {
|
532
|
mc_pre = And (List.map (translate_eexpr env) c.Lustre_types.assume);
|
533
|
mc_post = And (List.map (translate_eexpr env) c.Lustre_types.guarantees);
|
534
|
mc_proof = c.proof
|
535
|
}
|
536
|
|
537
|
let translate_spec env = function
|
538
|
| Contract c ->
|
539
|
Contract (translate_contract env c)
|
540
|
| NodeSpec s ->
|
541
|
NodeSpec s
|
542
|
|
543
|
let translate_decl nd sch =
|
544
|
(* Format.eprintf "Translating node %s@." nd.node_id; *)
|
545
|
(* Extracting eqs, variables .. *)
|
546
|
let eqs, auts = get_node_eqs nd in
|
547
|
assert (auts = []);
|
548
|
|
549
|
(* Automata should be expanded by now *)
|
550
|
|
551
|
(* In case of non functional backend (eg. C), additional local variables have
|
552
|
to be declared for each assert *)
|
553
|
let new_locals, assert_instrs, nd_node_asserts = process_asserts nd in
|
554
|
|
555
|
(* Build the env: variables visible in the current scope *)
|
556
|
let locals = nd.node_locals @ new_locals in
|
557
|
(* let locals = VSet.of_list locals_list in *)
|
558
|
(* let inout_vars = nd.node_inputs @ nd.node_outputs in *)
|
559
|
let env = build_env nd.node_inputs locals nd.node_outputs in
|
560
|
|
561
|
(* Format.eprintf "Node content is %a@." Printers.pp_node nd; *)
|
562
|
|
563
|
(* Computing main content *)
|
564
|
(* Format.eprintf "ok1@.@?"; *)
|
565
|
let schedule = sch.Scheduling_type.schedule in
|
566
|
(* Format.eprintf "ok2@.@?"; *)
|
567
|
let sorted_eqs, unused =
|
568
|
Scheduling.sort_equations_from_schedule eqs schedule
|
569
|
in
|
570
|
|
571
|
(* Format.eprintf "ok3@.locals=%a@.inout:%a@?"
|
572
|
* VSet.pp locals
|
573
|
* VSet.pp inout_vars
|
574
|
* ; *)
|
575
|
let equations = assert_instrs @ sorted_eqs in
|
576
|
let mems = get_memories env equations in
|
577
|
(* Removing computed memories from locals. We also removed unused variables. *)
|
578
|
let locals =
|
579
|
List.filter
|
580
|
(fun v -> (not (VSet.mem v mems)) && not (List.mem v.var_id unused))
|
581
|
locals
|
582
|
in
|
583
|
(* Compute live sets for spec *)
|
584
|
Lustre_live.set_live_of nd.node_id nd.node_outputs locals equations;
|
585
|
|
586
|
(* Translate equations *)
|
587
|
let ctx, ctx0_s =
|
588
|
translate_core env nd equations nd.node_inputs locals nd.node_outputs
|
589
|
in
|
590
|
|
591
|
(* Format.eprintf "ok4@.@?"; *)
|
592
|
|
593
|
(* Build the machine *)
|
594
|
let mmap = IMap.bindings ctx.j in
|
595
|
let mmemory_packs =
|
596
|
memory_pack_0 nd
|
597
|
::
|
598
|
List.mapi
|
599
|
(fun i f -> { mpname = nd; mpindex = Some (i + 1); mpformula = red f })
|
600
|
(List.rev ctx.mp)
|
601
|
@ [ memory_pack_toplevel nd (List.length ctx.mp) ]
|
602
|
in
|
603
|
let mtransitions =
|
604
|
transition_0 nd
|
605
|
::
|
606
|
List.mapi
|
607
|
(fun i (tvars, tmem_footprint, tinst_footprint, f) ->
|
608
|
{
|
609
|
tname = nd;
|
610
|
tindex = Some (i + 1);
|
611
|
tvars;
|
612
|
tformula = red f;
|
613
|
tmem_footprint;
|
614
|
tinst_footprint;
|
615
|
})
|
616
|
(List.rev ctx.t)
|
617
|
@ [ transition_toplevel nd (List.length ctx.t) ]
|
618
|
in
|
619
|
let clear_reset =
|
620
|
mkinstr
|
621
|
~instr_spec:
|
622
|
((if fst (get_stateless_status_node nd) then []
|
623
|
else [ mk_memory_pack ~i:0 nd.node_id ])
|
624
|
@ [ mk_transition ~i:0 nd.node_id (vdecls_to_vals nd.node_inputs) ])
|
625
|
MClearReset
|
626
|
in
|
627
|
let mnode_spec = Utils.option_map (translate_spec env) nd.node_spec in
|
628
|
{
|
629
|
mname = nd;
|
630
|
mmemory = VSet.elements mems;
|
631
|
mcalls = mmap;
|
632
|
minstances =
|
633
|
List.filter (fun (_, (n, _)) -> not (Stateless.check_node n)) mmap;
|
634
|
minit = List.rev ctx.si;
|
635
|
mconst = List.rev ctx0_s;
|
636
|
mstatic = List.filter (fun v -> v.var_dec_const) nd.node_inputs;
|
637
|
mstep =
|
638
|
{
|
639
|
step_inputs = nd.node_inputs;
|
640
|
step_outputs = nd.node_outputs;
|
641
|
step_locals = locals;
|
642
|
step_checks =
|
643
|
List.map
|
644
|
(fun d ->
|
645
|
d.Dimension.dim_loc, translate_expr env (expr_of_dimension d))
|
646
|
nd.node_checks;
|
647
|
step_instrs =
|
648
|
clear_reset
|
649
|
::
|
650
|
(* special treatment depending on the active backend. For horn
|
651
|
backend, common branches are not merged while they are in C or Java
|
652
|
backends. *)
|
653
|
(if !Backends.join_guards then join_guards_list (List.rev ctx.s)
|
654
|
else List.rev ctx.s);
|
655
|
step_asserts = List.map (translate_expr env) nd_node_asserts;
|
656
|
};
|
657
|
(* Processing spec: there is no processing performed here. Contract have
|
658
|
been processed already. Either one of the other machine is a cocospec
|
659
|
node, or the current one is a cocospec node. Contract do not contain any
|
660
|
statement or import. *)
|
661
|
mspec = { mnode_spec; mtransitions; mmemory_packs };
|
662
|
mannot = nd.node_annot;
|
663
|
msch = Some sch;
|
664
|
mis_contract = nd.node_iscontract
|
665
|
}
|
666
|
|
667
|
(** takes the global declarations and the scheduling associated to each node *)
|
668
|
let translate_prog decls node_schs =
|
669
|
let nodes = get_nodes decls in
|
670
|
let machines =
|
671
|
List.map
|
672
|
(fun decl ->
|
673
|
let node = node_of_top decl in
|
674
|
let sch = IMap.find node.node_id node_schs in
|
675
|
translate_decl node sch)
|
676
|
nodes
|
677
|
in
|
678
|
machines
|
679
|
|
680
|
(* Local Variables: *)
|
681
|
(* compile-command:"make -C .." *)
|
682
|
(* End: *)
|