1
|
|
2
|
(* ----------------------------------------------------------------------------
|
3
|
* SchedMCore - A MultiCore Scheduling Framework
|
4
|
* Copyright (C) 2009-2013, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE
|
5
|
* Copyright (C) 2012-2013, INPT, Toulouse, FRANCE
|
6
|
*
|
7
|
* This file is part of Prelude
|
8
|
*
|
9
|
* Prelude is free software; you can redistribute it and/or
|
10
|
* modify it under the terms of the GNU Lesser General Public License
|
11
|
* as published by the Free Software Foundation ; either version 2 of
|
12
|
* the License, or (at your option) any later version.
|
13
|
*
|
14
|
* Prelude is distributed in the hope that it will be useful, but
|
15
|
* WITHOUT ANY WARRANTY ; without even the implied warranty of
|
16
|
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
|
17
|
* Lesser General Public License for more details.
|
18
|
*
|
19
|
* You should have received a copy of the GNU Lesser General Public
|
20
|
* License along with this program ; if not, write to the Free Software
|
21
|
* Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
|
22
|
* USA
|
23
|
*---------------------------------------------------------------------------- *)
|
24
|
|
25
|
(* This module is used for the lustre to C compiler *)
|
26
|
|
27
|
open LustreSpec
|
28
|
open Corelang
|
29
|
open Clocks
|
30
|
open Causality
|
31
|
|
32
|
exception NormalizationError
|
33
|
|
34
|
module OrdVarDecl:Map.OrderedType with type t=var_decl =
|
35
|
struct type t = var_decl;; let compare = compare end
|
36
|
|
37
|
module ISet = Set.Make(OrdVarDecl)
|
38
|
|
39
|
type value_t =
|
40
|
| Cst of constant
|
41
|
| LocalVar of var_decl
|
42
|
| StateVar of var_decl
|
43
|
| Fun of ident * value_t list
|
44
|
| Array of value_t list
|
45
|
| Access of value_t * value_t
|
46
|
| Power of value_t * value_t
|
47
|
|
48
|
type instr_t =
|
49
|
| MLocalAssign of var_decl * value_t
|
50
|
| MStateAssign of var_decl * value_t
|
51
|
| MReset of ident
|
52
|
| MStep of var_decl list * ident * value_t list
|
53
|
| MBranch of value_t * (label * instr_t list) list
|
54
|
|
55
|
let rec pp_val fmt v =
|
56
|
match v with
|
57
|
| Cst c -> Printers.pp_const fmt c
|
58
|
| LocalVar v -> Format.pp_print_string fmt v.var_id
|
59
|
| StateVar v -> Format.pp_print_string fmt v.var_id
|
60
|
| Array vl -> Format.fprintf fmt "[%a]" (Utils.fprintf_list ~sep:", " pp_val) vl
|
61
|
| Access (t, i) -> Format.fprintf fmt "%a[%a]" pp_val t pp_val i
|
62
|
| Power (v, n) -> Format.fprintf fmt "(%a^%a)" pp_val v pp_val n
|
63
|
| Fun (n, vl) -> Format.fprintf fmt "%s (%a)" n (Utils.fprintf_list ~sep:", " pp_val) vl
|
64
|
|
65
|
let rec pp_instr fmt i =
|
66
|
match i with
|
67
|
| MLocalAssign (i,v) -> Format.fprintf fmt "%s<-l- %a" i.var_id pp_val v
|
68
|
| MStateAssign (i,v) -> Format.fprintf fmt "%s<-s- %a" i.var_id pp_val v
|
69
|
| MReset i -> Format.fprintf fmt "reset %s" i
|
70
|
| MStep (il, i, vl) ->
|
71
|
Format.fprintf fmt "%a = %s (%a)"
|
72
|
(Utils.fprintf_list ~sep:", " (fun fmt v -> Format.pp_print_string fmt v.var_id)) il
|
73
|
i
|
74
|
(Utils.fprintf_list ~sep:", " pp_val) vl
|
75
|
| MBranch (g,hl) ->
|
76
|
Format.fprintf fmt "@[<v 2>case(%a) {@,%a@,}@]"
|
77
|
pp_val g
|
78
|
(Utils.fprintf_list ~sep:"@," pp_branch) hl
|
79
|
|
80
|
and pp_branch fmt (t, h) =
|
81
|
Format.fprintf fmt "@[<v 2>%s:@,%a@]" t (Utils.fprintf_list ~sep:"@," pp_instr) h
|
82
|
|
83
|
type step_t = {
|
84
|
step_checks: (Location.t * value_t) list;
|
85
|
step_inputs: var_decl list;
|
86
|
step_outputs: var_decl list;
|
87
|
step_locals: var_decl list;
|
88
|
step_instrs: instr_t list;
|
89
|
step_asserts: value_t list;
|
90
|
}
|
91
|
|
92
|
type static_call = top_decl * (Dimension.dim_expr list)
|
93
|
|
94
|
type machine_t = {
|
95
|
mname: node_desc;
|
96
|
mmemory: var_decl list;
|
97
|
mcalls: (ident * static_call) list; (* map from stateful/stateless instance to node, no internals *)
|
98
|
minstances: (ident * static_call) list; (* sub-map of mcalls, from stateful instance to node *)
|
99
|
minit: instr_t list;
|
100
|
mstatic: var_decl list; (* static inputs only *)
|
101
|
mstep: step_t;
|
102
|
mspec: node_annot option;
|
103
|
mannot: expr_annot list;
|
104
|
}
|
105
|
|
106
|
let pp_step fmt s =
|
107
|
Format.fprintf fmt "@[<v>inputs : %a@ outputs: %a@ locals : %a@ checks : %a@ instrs : @[%a@]@ asserts : @[%a@]@]@ "
|
108
|
(Utils.fprintf_list ~sep:", " Printers.pp_var) s.step_inputs
|
109
|
(Utils.fprintf_list ~sep:", " Printers.pp_var) s.step_outputs
|
110
|
(Utils.fprintf_list ~sep:", " Printers.pp_var) s.step_locals
|
111
|
(Utils.fprintf_list ~sep:", " (fun fmt (_, c) -> pp_val fmt c)) s.step_checks
|
112
|
(Utils.fprintf_list ~sep:"@ " pp_instr) s.step_instrs
|
113
|
(Utils.fprintf_list ~sep:", " pp_val) s.step_asserts
|
114
|
|
115
|
|
116
|
let pp_static_call fmt (node, args) =
|
117
|
Format.fprintf fmt "%s<%a>"
|
118
|
(node_name node)
|
119
|
(Utils.fprintf_list ~sep:", " Dimension.pp_dimension) args
|
120
|
|
121
|
let pp_machine fmt m =
|
122
|
Format.fprintf fmt
|
123
|
"@[<v 2>machine %s@ mem : %a@ instances: %a@ init : %a@ step :@ @[<v 2>%a@]@ @ spec : @[%t@]@ annot : @[%a@]@]@ "
|
124
|
m.mname.node_id
|
125
|
(Utils.fprintf_list ~sep:", " Printers.pp_var) m.mmemory
|
126
|
(Utils.fprintf_list ~sep:", " (fun fmt (o1, o2) -> Format.fprintf fmt "(%s, %a)" o1 pp_static_call o2)) m.minstances
|
127
|
(Utils.fprintf_list ~sep:"@ " pp_instr) m.minit
|
128
|
pp_step m.mstep
|
129
|
(fun fmt -> match m.mspec with | None -> () | Some spec -> Printers.pp_spec fmt spec)
|
130
|
(Utils.fprintf_list ~sep:"@ " Printers.pp_expr_annot) m.mannot
|
131
|
|
132
|
(* Returns the declared stateless status and the computed one. *)
|
133
|
let get_stateless_status m =
|
134
|
(m.mname.node_dec_stateless, Utils.desome m.mname.node_stateless)
|
135
|
|
136
|
let is_input m id =
|
137
|
List.exists (fun o -> o.var_id = id.var_id) m.mstep.step_inputs
|
138
|
|
139
|
let is_output m id =
|
140
|
List.exists (fun o -> o.var_id = id.var_id) m.mstep.step_outputs
|
141
|
|
142
|
let is_memory m id =
|
143
|
List.exists (fun o -> o.var_id = id.var_id) m.mmemory
|
144
|
|
145
|
let conditional c t e =
|
146
|
MBranch(c, [ (tag_true, t); (tag_false, e) ])
|
147
|
|
148
|
let dummy_var_decl name typ =
|
149
|
{
|
150
|
var_id = name;
|
151
|
var_dec_type = dummy_type_dec;
|
152
|
var_dec_clock = dummy_clock_dec;
|
153
|
var_dec_const = false;
|
154
|
var_type = typ;
|
155
|
var_clock = Clocks.new_ck (Clocks.Cvar Clocks.CSet_all) true;
|
156
|
var_loc = Location.dummy_loc
|
157
|
}
|
158
|
|
159
|
let arrow_id = "_arrow"
|
160
|
|
161
|
let arrow_typ = Types.new_ty Types.Tunivar
|
162
|
|
163
|
let arrow_desc =
|
164
|
{
|
165
|
node_id = arrow_id;
|
166
|
node_type = Type_predef.type_bin_poly_op;
|
167
|
node_clock = Clock_predef.ck_bin_univ;
|
168
|
node_inputs= [dummy_var_decl "_in1" arrow_typ; dummy_var_decl "_in2" arrow_typ];
|
169
|
node_outputs= [dummy_var_decl "_out" arrow_typ];
|
170
|
node_locals= [];
|
171
|
node_gencalls = [];
|
172
|
node_checks = [];
|
173
|
node_asserts = [];
|
174
|
node_eqs= [];
|
175
|
node_dec_stateless = false;
|
176
|
node_stateless = Some false;
|
177
|
node_spec = None;
|
178
|
node_annot = []; }
|
179
|
|
180
|
let arrow_top_decl =
|
181
|
{
|
182
|
top_decl_desc = Node arrow_desc;
|
183
|
top_decl_loc = Location.dummy_loc
|
184
|
}
|
185
|
|
186
|
let arrow_machine =
|
187
|
let state = "_first" in
|
188
|
let var_state = dummy_var_decl state (Types.new_ty Types.Tbool) in
|
189
|
let var_input1 = List.nth arrow_desc.node_inputs 0 in
|
190
|
let var_input2 = List.nth arrow_desc.node_inputs 1 in
|
191
|
let var_output = List.nth arrow_desc.node_outputs 0 in
|
192
|
{
|
193
|
mname = arrow_desc;
|
194
|
mmemory = [var_state];
|
195
|
mcalls = [];
|
196
|
minstances = [];
|
197
|
minit = [MStateAssign(var_state, Cst (const_of_bool true))];
|
198
|
mstatic = [];
|
199
|
mstep = {
|
200
|
step_inputs = arrow_desc.node_inputs;
|
201
|
step_outputs = arrow_desc.node_outputs;
|
202
|
step_locals = [];
|
203
|
step_checks = [];
|
204
|
step_instrs = [conditional (StateVar var_state)
|
205
|
[MStateAssign(var_state, Cst (const_of_bool false));
|
206
|
MLocalAssign(var_output, LocalVar var_input1)]
|
207
|
[MLocalAssign(var_output, LocalVar var_input2)] ];
|
208
|
step_asserts = [];
|
209
|
};
|
210
|
mspec = None;
|
211
|
mannot = [];
|
212
|
}
|
213
|
|
214
|
let new_instance =
|
215
|
let cpt = ref (-1) in
|
216
|
fun caller callee tag ->
|
217
|
begin
|
218
|
let o =
|
219
|
if Stateless.check_node callee then
|
220
|
node_name callee
|
221
|
else
|
222
|
Printf.sprintf "ni_%d" (incr cpt; !cpt) in
|
223
|
let o =
|
224
|
if !Options.ansi && is_generic_node callee
|
225
|
then Printf.sprintf "%s_inst_%d" o (Utils.position (fun e -> e.expr_tag = tag) caller.node_gencalls)
|
226
|
else o in
|
227
|
o
|
228
|
end
|
229
|
|
230
|
(* translate_<foo> : node -> context -> <foo> -> machine code/expression *)
|
231
|
(* the context contains m : state aka memory variables *)
|
232
|
(* si : initialization instructions *)
|
233
|
(* j : node aka machine instances *)
|
234
|
(* d : local variables *)
|
235
|
(* s : step instructions *)
|
236
|
let translate_ident node (m, si, j, d, s) id =
|
237
|
try (* id is a node var *)
|
238
|
let var_id = get_node_var id node in
|
239
|
if ISet.exists (fun v -> v.var_id = id) m
|
240
|
then StateVar var_id
|
241
|
else LocalVar var_id
|
242
|
with Not_found -> (* id is a constant *)
|
243
|
LocalVar (Corelang.var_decl_of_const (Hashtbl.find Corelang.consts_table id))
|
244
|
|
245
|
let rec control_on_clock node ((m, si, j, d, s) as args) ck inst =
|
246
|
match (Clocks.repr ck).cdesc with
|
247
|
| Con (ck1, cr, l) ->
|
248
|
let id = Clocks.const_of_carrier cr in
|
249
|
control_on_clock node args ck1 (MBranch (translate_ident node args id,
|
250
|
[l, [inst]] ))
|
251
|
| _ -> inst
|
252
|
|
253
|
let rec join_branches hl1 hl2 =
|
254
|
match hl1, hl2 with
|
255
|
| [] , _ -> hl2
|
256
|
| _ , [] -> hl1
|
257
|
| (t1, h1)::q1, (t2, h2)::q2 ->
|
258
|
if t1 < t2 then (t1, h1) :: join_branches q1 hl2 else
|
259
|
if t1 > t2 then (t2, h2) :: join_branches hl1 q2
|
260
|
else (t1, List.fold_right join_guards h1 h2) :: join_branches q1 q2
|
261
|
|
262
|
and join_guards inst1 insts2 =
|
263
|
match inst1, insts2 with
|
264
|
| _ , [] ->
|
265
|
[inst1]
|
266
|
| MBranch (x1, hl1), MBranch (x2, hl2) :: q when x1 = x2 ->
|
267
|
MBranch (x1, join_branches (sort_handlers hl1) (sort_handlers hl2))
|
268
|
:: q
|
269
|
| _ -> inst1 :: insts2
|
270
|
|
271
|
let join_guards_list insts =
|
272
|
List.fold_right join_guards insts []
|
273
|
|
274
|
let find_eq x eqs =
|
275
|
let rec aux accu eqs =
|
276
|
match eqs with
|
277
|
| [] ->
|
278
|
begin
|
279
|
Format.eprintf "Looking for variable %a in the following equations@.%a@."
|
280
|
Format.pp_print_string x
|
281
|
Printers.pp_node_eqs eqs;
|
282
|
assert false
|
283
|
end
|
284
|
| hd::tl ->
|
285
|
if List.mem x hd.eq_lhs then hd, accu@tl else aux (hd::accu) tl
|
286
|
in
|
287
|
aux [] eqs
|
288
|
|
289
|
(* specialize predefined (polymorphic) operators
|
290
|
wrt their instances, so that the C semantics
|
291
|
is preserved *)
|
292
|
let specialize_to_c expr =
|
293
|
match expr.expr_desc with
|
294
|
| Expr_appl (id, e, r) ->
|
295
|
if List.exists (fun e -> Types.is_bool_type e.expr_type) (expr_list_of_expr e)
|
296
|
then let id =
|
297
|
match id with
|
298
|
| "=" -> "equi"
|
299
|
| "!=" -> "xor"
|
300
|
| _ -> id in
|
301
|
{ expr with expr_desc = Expr_appl (id, e, r) }
|
302
|
else expr
|
303
|
| _ -> expr
|
304
|
|
305
|
let specialize_op expr =
|
306
|
match !Options.output with
|
307
|
| "C" -> specialize_to_c expr
|
308
|
| _ -> expr
|
309
|
|
310
|
let rec translate_expr node ((m, si, j, d, s) as args) expr =
|
311
|
let expr = specialize_op expr in
|
312
|
match expr.expr_desc with
|
313
|
| Expr_const v -> Cst v
|
314
|
| Expr_ident x -> translate_ident node args x
|
315
|
| Expr_array el -> Array (List.map (translate_expr node args) el)
|
316
|
| Expr_access (t, i) -> Access (translate_expr node args t, translate_expr node args (expr_of_dimension i))
|
317
|
| Expr_power (e, n) -> Power (translate_expr node args e, translate_expr node args (expr_of_dimension n))
|
318
|
| Expr_tuple _
|
319
|
| Expr_arrow _
|
320
|
| Expr_fby _
|
321
|
| Expr_pre _ -> (Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError)
|
322
|
| Expr_when (e1, _, _) -> translate_expr node args e1
|
323
|
| Expr_merge (x, _) -> raise NormalizationError
|
324
|
| Expr_appl (id, e, _) when Basic_library.is_internal_fun id ->
|
325
|
let nd = node_from_name id in
|
326
|
Fun (node_name nd, List.map (translate_expr node args) (expr_list_of_expr e))
|
327
|
| Expr_ite (g,t,e) -> (
|
328
|
(* special treatment depending on the active backend. For horn backend, ite
|
329
|
are preserved in expression. While they are removed for C or Java
|
330
|
backends. *)
|
331
|
match !Options.output with | "horn" ->
|
332
|
Fun ("ite", [translate_expr node args g; translate_expr node args t; translate_expr node args e])
|
333
|
| "C" | "java" | _ ->
|
334
|
(Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError)
|
335
|
)
|
336
|
| _ -> raise NormalizationError
|
337
|
|
338
|
let translate_guard node args expr =
|
339
|
match expr.expr_desc with
|
340
|
| Expr_ident x -> translate_ident node args x
|
341
|
| _ -> (Format.eprintf "internal error: translate_guard %s %a@." node.node_id Printers.pp_expr expr;assert false)
|
342
|
|
343
|
let rec translate_act node ((m, si, j, d, s) as args) (y, expr) =
|
344
|
match expr.expr_desc with
|
345
|
| Expr_ite (c, t, e) -> let g = translate_guard node args c in
|
346
|
conditional g [translate_act node args (y, t)]
|
347
|
[translate_act node args (y, e)]
|
348
|
| Expr_merge (x, hl) -> MBranch (translate_ident node args x, List.map (fun (t, h) -> t, [translate_act node args (y, h)]) hl)
|
349
|
| _ -> MLocalAssign (y, translate_expr node args expr)
|
350
|
|
351
|
let reset_instance node args i r c =
|
352
|
match r with
|
353
|
| None -> []
|
354
|
| Some (x, l) -> [control_on_clock node args c (MBranch (translate_ident node args x, [l, [MReset i]]))]
|
355
|
|
356
|
let translate_eq node ((m, si, j, d, s) as args) eq =
|
357
|
(*Format.eprintf "translate_eq %a with clock %a@." Printers.pp_node_eq eq Clocks.print_ck eq.eq_rhs.expr_clock;*)
|
358
|
match eq.eq_lhs, eq.eq_rhs.expr_desc with
|
359
|
| [x], Expr_arrow (e1, e2) ->
|
360
|
let var_x = get_node_var x node in
|
361
|
let o = new_instance node arrow_top_decl eq.eq_rhs.expr_tag in
|
362
|
let c1 = translate_expr node args e1 in
|
363
|
let c2 = translate_expr node args e2 in
|
364
|
(m,
|
365
|
MReset o :: si,
|
366
|
Utils.IMap.add o (arrow_top_decl, []) j,
|
367
|
d,
|
368
|
(control_on_clock node args eq.eq_rhs.expr_clock (MStep ([var_x], o, [c1;c2]))) :: s)
|
369
|
| [x], Expr_pre e1 when ISet.mem (get_node_var x node) d ->
|
370
|
let var_x = get_node_var x node in
|
371
|
(ISet.add var_x m,
|
372
|
si,
|
373
|
j,
|
374
|
d,
|
375
|
control_on_clock node args eq.eq_rhs.expr_clock (MStateAssign (var_x, translate_expr node args e1)) :: s)
|
376
|
| [x], Expr_fby (e1, e2) when ISet.mem (get_node_var x node) d ->
|
377
|
let var_x = get_node_var x node in
|
378
|
(ISet.add var_x m,
|
379
|
MStateAssign (var_x, translate_expr node args e1) :: si,
|
380
|
j,
|
381
|
d,
|
382
|
control_on_clock node args eq.eq_rhs.expr_clock (MStateAssign (var_x, translate_expr node args e2)) :: s)
|
383
|
|
384
|
| p , Expr_appl (f, arg, r) when not (Basic_library.is_internal_fun f) ->
|
385
|
let var_p = List.map (fun v -> get_node_var v node) p in
|
386
|
let el = expr_list_of_expr arg in
|
387
|
let vl = List.map (translate_expr node args) el in
|
388
|
let node_f = node_from_name f in
|
389
|
let call_f =
|
390
|
node_f,
|
391
|
NodeDep.filter_static_inputs (node_inputs node_f) el in
|
392
|
let o = new_instance node node_f eq.eq_rhs.expr_tag in
|
393
|
let call_ck = Clocks.new_var true in
|
394
|
Clock_calculus.unify_imported_clock (Some call_ck) eq.eq_rhs.expr_clock;
|
395
|
(m,
|
396
|
(if Stateless.check_node node_f then si else MReset o :: si),
|
397
|
Utils.IMap.add o call_f j,
|
398
|
d,
|
399
|
reset_instance node args o r eq.eq_rhs.expr_clock @
|
400
|
(control_on_clock node args call_ck (MStep (var_p, o, vl))) :: s)
|
401
|
|
402
|
(* special treatment depending on the active backend. For horn backend, x = ite (g,t,e)
|
403
|
are preserved. While they are replaced as if g then x = t else x = e in C or Java
|
404
|
backends. *)
|
405
|
| [x], Expr_ite (c, t, e)
|
406
|
when (match !Options.output with | "horn" -> true | "C" | "java" | _ -> false)
|
407
|
->
|
408
|
let var_x = get_node_var x node in
|
409
|
(m,
|
410
|
si,
|
411
|
j,
|
412
|
d,
|
413
|
(control_on_clock node args eq.eq_rhs.expr_clock
|
414
|
(MLocalAssign (var_x, translate_expr node args eq.eq_rhs))::s)
|
415
|
)
|
416
|
|
417
|
| [x], _ -> (
|
418
|
let var_x = get_node_var x node in
|
419
|
(m, si, j, d,
|
420
|
control_on_clock
|
421
|
node
|
422
|
args
|
423
|
eq.eq_rhs.expr_clock
|
424
|
(translate_act node args (var_x, eq.eq_rhs)) :: s
|
425
|
)
|
426
|
)
|
427
|
| _ ->
|
428
|
begin
|
429
|
Format.eprintf "unsupported equation: %a@?" Printers.pp_node_eq eq;
|
430
|
assert false
|
431
|
end
|
432
|
|
433
|
let translate_eqs node args eqs =
|
434
|
List.fold_right (fun eq args -> translate_eq node args eq) eqs args;;
|
435
|
|
436
|
let translate_decl nd sch =
|
437
|
(*Log.report ~level:1 (fun fmt -> Printers.pp_node fmt nd);*)
|
438
|
let split_eqs = Splitting.tuple_split_eq_list nd.node_eqs in
|
439
|
let eqs_rev, remainder =
|
440
|
List.fold_left
|
441
|
(fun (accu, node_eqs_remainder) v ->
|
442
|
if List.exists (fun eq -> List.mem v eq.eq_lhs) accu
|
443
|
then
|
444
|
(accu, node_eqs_remainder)
|
445
|
else
|
446
|
(*if List.exists (fun vdecl -> vdecl.var_id = v) nd.node_locals
|
447
|
|| List.exists (fun vdecl -> vdecl.var_id = v) nd.node_outputs
|
448
|
then*)
|
449
|
let eq_v, remainder = find_eq v node_eqs_remainder in
|
450
|
eq_v::accu, remainder
|
451
|
(* else it is a constant value, checked during typing phase
|
452
|
else
|
453
|
accu, node_eqs_remainder *)
|
454
|
)
|
455
|
([], split_eqs)
|
456
|
sch
|
457
|
in
|
458
|
if List.length remainder > 0 then (
|
459
|
Format.eprintf "Equations not used are@.%a@.Full equation set is:@.%a@.@?"
|
460
|
Printers.pp_node_eqs remainder
|
461
|
Printers.pp_node_eqs nd.node_eqs;
|
462
|
assert false )
|
463
|
;
|
464
|
|
465
|
let init_args = ISet.empty, [], Utils.IMap.empty, List.fold_right (fun l -> ISet.add l) nd.node_locals ISet.empty, [] in
|
466
|
(* memories, init instructions, node calls, local variables (including memories), step instrs *)
|
467
|
let m, init, j, locals, s = translate_eqs nd init_args (List.rev eqs_rev) in
|
468
|
let mmap = Utils.IMap.fold (fun i n res -> (i, n)::res) j [] in
|
469
|
{
|
470
|
mname = nd;
|
471
|
mmemory = ISet.elements m;
|
472
|
mcalls = mmap;
|
473
|
minstances = List.filter (fun (_, (n,_)) -> not (Stateless.check_node n)) mmap;
|
474
|
minit = init;
|
475
|
mstatic = List.filter (fun v -> v.var_dec_const) nd.node_inputs;
|
476
|
mstep = {
|
477
|
step_inputs = nd.node_inputs;
|
478
|
step_outputs = nd.node_outputs;
|
479
|
step_locals = ISet.elements (ISet.diff locals m);
|
480
|
step_checks = List.map (fun d -> d.Dimension.dim_loc, translate_expr nd init_args (expr_of_dimension d)) nd.node_checks;
|
481
|
step_instrs = (
|
482
|
(* special treatment depending on the active backend. For horn backend,
|
483
|
common branches are not merged while they are in C or Java
|
484
|
backends. *)
|
485
|
match !Options.output with
|
486
|
| "horn" -> s
|
487
|
| "C" | "java" | _ -> join_guards_list s
|
488
|
);
|
489
|
step_asserts =
|
490
|
let exprl = List.map (fun assert_ -> assert_.assert_expr ) nd.node_asserts in
|
491
|
List.map (translate_expr nd init_args) exprl
|
492
|
;
|
493
|
};
|
494
|
mspec = nd.node_spec;
|
495
|
mannot = nd.node_annot;
|
496
|
}
|
497
|
|
498
|
(** takes the global delcarations and the scheduling associated to each node *)
|
499
|
let translate_prog decls node_schs =
|
500
|
let nodes = get_nodes decls in
|
501
|
List.map
|
502
|
(fun node ->
|
503
|
let sch = (Utils.IMap.find node.node_id node_schs).Scheduling.schedule in
|
504
|
translate_decl node sch
|
505
|
) nodes
|
506
|
|
507
|
let get_machine_opt name machines =
|
508
|
List.fold_left
|
509
|
(fun res m ->
|
510
|
match res with
|
511
|
| Some _ -> res
|
512
|
| None -> if m.mname.node_id = name then Some m else None)
|
513
|
None machines
|
514
|
|
515
|
(* variable substitution for optimizing purposes *)
|
516
|
|
517
|
(* checks whether an [instr] is skip and can be removed from program *)
|
518
|
let rec instr_is_skip instr =
|
519
|
match instr with
|
520
|
| MLocalAssign (i, LocalVar v) when i = v -> true
|
521
|
| MStateAssign (i, StateVar v) when i = v -> true
|
522
|
| MBranch (g, hl) -> List.for_all (fun (_, il) -> instrs_are_skip il) hl
|
523
|
| _ -> false
|
524
|
and instrs_are_skip instrs =
|
525
|
List.for_all instr_is_skip instrs
|
526
|
|
527
|
let rec instr_remove_skip instr cont =
|
528
|
match instr with
|
529
|
| MLocalAssign (i, LocalVar v) when i = v -> cont
|
530
|
| MStateAssign (i, StateVar v) when i = v -> cont
|
531
|
| MBranch (g, hl) -> MBranch (g, List.map (fun (h, il) -> (h, instrs_remove_skip il [])) hl) :: cont
|
532
|
| _ -> instr::cont
|
533
|
|
534
|
and instrs_remove_skip instrs cont =
|
535
|
List.fold_right instr_remove_skip instrs cont
|
536
|
|
537
|
let rec value_replace_var fvar value =
|
538
|
match value with
|
539
|
| Cst c -> value
|
540
|
| LocalVar v -> LocalVar (fvar v)
|
541
|
| StateVar v -> value
|
542
|
| Fun (id, args) -> Fun (id, List.map (value_replace_var fvar) args)
|
543
|
| Array vl -> Array (List.map (value_replace_var fvar) vl)
|
544
|
| Access (t, i) -> Access(value_replace_var fvar t, i)
|
545
|
| Power (v, n) -> Power(value_replace_var fvar v, n)
|
546
|
|
547
|
let rec instr_replace_var fvar instr =
|
548
|
match instr with
|
549
|
| MLocalAssign (i, v) -> MLocalAssign (fvar i, value_replace_var fvar v)
|
550
|
| MStateAssign (i, v) -> MStateAssign (i, value_replace_var fvar v)
|
551
|
| MReset i -> instr
|
552
|
| MStep (il, i, vl) -> MStep (List.map fvar il, i, List.map (value_replace_var fvar) vl)
|
553
|
| MBranch (g, hl) -> MBranch (value_replace_var fvar g, List.map (fun (h, il) -> (h, instrs_replace_var fvar il)) hl)
|
554
|
|
555
|
and instrs_replace_var fvar instrs =
|
556
|
List.map (instr_replace_var fvar) instrs
|
557
|
|
558
|
let step_replace_var fvar step =
|
559
|
{ step with
|
560
|
step_checks = List.map (fun (l, v) -> (l, value_replace_var fvar v)) step.step_checks;
|
561
|
step_locals = Utils.remove_duplicates (List.map fvar step.step_locals);
|
562
|
step_instrs = instrs_replace_var fvar step.step_instrs;
|
563
|
}
|
564
|
|
565
|
let rec machine_replace_var fvar m =
|
566
|
{ m with
|
567
|
mstep = step_replace_var fvar m.mstep
|
568
|
}
|
569
|
|
570
|
let machine_reuse_var m reuse =
|
571
|
let reuse_vdecl = Hashtbl.create 23 in
|
572
|
begin
|
573
|
Hashtbl.iter (fun v v' -> Hashtbl.add reuse_vdecl (get_node_var v m.mname) (get_node_var v' m.mname)) reuse;
|
574
|
let fvar v =
|
575
|
try
|
576
|
Hashtbl.find reuse_vdecl v
|
577
|
with Not_found -> v in
|
578
|
machine_replace_var fvar m
|
579
|
end
|
580
|
|
581
|
let prog_reuse_var prog node_schs =
|
582
|
List.map
|
583
|
(fun m ->
|
584
|
machine_reuse_var m (Utils.IMap.find m.mname.node_id node_schs).Scheduling.reuse_table
|
585
|
) prog
|
586
|
|
587
|
(* Local Variables: *)
|
588
|
(* compile-command:"make -C .." *)
|
589
|
(* End: *)
|