lustrec / src / machine_code.ml @ 3ca27bc7
History | View | Annotate | Download (26.4 KB)
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 LustreSpec |
13 |
open Corelang |
14 |
open Clocks |
15 |
open Causality |
16 |
|
17 |
let print_statelocaltag = true |
18 |
|
19 |
exception NormalizationError |
20 |
|
21 |
module OrdVarDecl:Map.OrderedType with type t=var_decl = |
22 |
struct type t = var_decl;; let compare = compare end |
23 |
|
24 |
module ISet = Set.Make(OrdVarDecl) |
25 |
|
26 |
let rec pp_val fmt v = |
27 |
match v.value_desc with |
28 |
| Cst c -> Printers.pp_const fmt c |
29 |
| LocalVar v -> |
30 |
if print_statelocaltag then |
31 |
Format.fprintf fmt "%s(L)" v.var_id |
32 |
else |
33 |
Format.pp_print_string fmt v.var_id |
34 |
|
35 |
| StateVar v -> |
36 |
if print_statelocaltag then |
37 |
Format.fprintf fmt "%s(S)" v.var_id |
38 |
else |
39 |
Format.pp_print_string fmt v.var_id |
40 |
| Array vl -> Format.fprintf fmt "[%a]" (Utils.fprintf_list ~sep:", " pp_val) vl |
41 |
| Access (t, i) -> Format.fprintf fmt "%a[%a]" pp_val t pp_val i |
42 |
| Power (v, n) -> Format.fprintf fmt "(%a^%a)" pp_val v pp_val n |
43 |
| Fun (n, vl) -> Format.fprintf fmt "%s (%a)" n (Utils.fprintf_list ~sep:", " pp_val) vl |
44 |
|
45 |
let rec pp_instr fmt i = |
46 |
match i.instr_desc with |
47 |
| MLocalAssign (i,v) -> Format.fprintf fmt "%s<-l- %a" i.var_id pp_val v |
48 |
| MStateAssign (i,v) -> Format.fprintf fmt "%s<-s- %a" i.var_id pp_val v |
49 |
| MReset i -> Format.fprintf fmt "reset %s" i |
50 |
| MNoReset i -> Format.fprintf fmt "noreset %s" i |
51 |
| MStep (il, i, vl) -> |
52 |
Format.fprintf fmt "%a = %s (%a)" |
53 |
(Utils.fprintf_list ~sep:", " (fun fmt v -> Format.pp_print_string fmt v.var_id)) il |
54 |
i |
55 |
(Utils.fprintf_list ~sep:", " pp_val) vl |
56 |
| MBranch (g,hl) -> |
57 |
Format.fprintf fmt "@[<v 2>case(%a) {@,%a@,}@]" |
58 |
pp_val g |
59 |
(Utils.fprintf_list ~sep:"@," pp_branch) hl |
60 |
| MComment s -> Format.pp_print_string fmt s |
61 |
|
62 |
and pp_branch fmt (t, h) = |
63 |
Format.fprintf fmt "@[<v 2>%s:@,%a@]" t (Utils.fprintf_list ~sep:"@," pp_instr) h |
64 |
|
65 |
and pp_instrs fmt il = |
66 |
Format.fprintf fmt "@[<v 2>%a@]" (Utils.fprintf_list ~sep:"@," pp_instr) il |
67 |
|
68 |
type step_t = { |
69 |
step_checks: (Location.t * value_t) list; |
70 |
step_inputs: var_decl list; |
71 |
step_outputs: var_decl list; |
72 |
step_locals: var_decl list; |
73 |
step_instrs: instr_t list; |
74 |
step_asserts: value_t list; |
75 |
} |
76 |
|
77 |
type static_call = top_decl * (Dimension.dim_expr list) |
78 |
|
79 |
type machine_t = { |
80 |
mname: node_desc; |
81 |
mmemory: var_decl list; |
82 |
mcalls: (ident * static_call) list; (* map from stateful/stateless instance to node, no internals *) |
83 |
minstances: (ident * static_call) list; (* sub-map of mcalls, from stateful instance to node *) |
84 |
minit: instr_t list; |
85 |
mstatic: var_decl list; (* static inputs only *) |
86 |
mconst: instr_t list; (* assignments of node constant locals *) |
87 |
mstep: step_t; |
88 |
mspec: node_annot option; |
89 |
mannot: expr_annot list; |
90 |
} |
91 |
|
92 |
(* merge log: get_node_def was in c0f8 *) |
93 |
let get_node_def id m = |
94 |
try |
95 |
let (decl, _) = List.assoc id m.minstances in |
96 |
Corelang.node_of_top decl |
97 |
with Not_found -> raise Not_found |
98 |
|
99 |
(* merge log: machine_vars was in 44686 *) |
100 |
let machine_vars m = m.mstep.step_inputs @ m.mstep.step_locals @ m.mstep.step_outputs @ m.mmemory |
101 |
|
102 |
let pp_step fmt s = |
103 |
Format.fprintf fmt "@[<v>inputs : %a@ outputs: %a@ locals : %a@ checks : %a@ instrs : @[%a@]@ asserts : @[%a@]@]@ " |
104 |
(Utils.fprintf_list ~sep:", " Printers.pp_var) s.step_inputs |
105 |
(Utils.fprintf_list ~sep:", " Printers.pp_var) s.step_outputs |
106 |
(Utils.fprintf_list ~sep:", " Printers.pp_var) s.step_locals |
107 |
(Utils.fprintf_list ~sep:", " (fun fmt (_, c) -> pp_val fmt c)) s.step_checks |
108 |
(Utils.fprintf_list ~sep:"@ " pp_instr) s.step_instrs |
109 |
(Utils.fprintf_list ~sep:", " pp_val) s.step_asserts |
110 |
|
111 |
|
112 |
let pp_static_call fmt (node, args) = |
113 |
Format.fprintf fmt "%s<%a>" |
114 |
(node_name node) |
115 |
(Utils.fprintf_list ~sep:", " Dimension.pp_dimension) args |
116 |
|
117 |
let pp_machine fmt m = |
118 |
Format.fprintf fmt |
119 |
"@[<v 2>machine %s@ mem : %a@ instances: %a@ init : %a@ const : %a@ step :@ @[<v 2>%a@]@ @ spec : @[%t@]@ annot : @[%a@]@]@ " |
120 |
m.mname.node_id |
121 |
(Utils.fprintf_list ~sep:", " Printers.pp_var) m.mmemory |
122 |
(Utils.fprintf_list ~sep:", " (fun fmt (o1, o2) -> Format.fprintf fmt "(%s, %a)" o1 pp_static_call o2)) m.minstances |
123 |
(Utils.fprintf_list ~sep:"@ " pp_instr) m.minit |
124 |
(Utils.fprintf_list ~sep:"@ " pp_instr) m.mconst |
125 |
pp_step m.mstep |
126 |
(fun fmt -> match m.mspec with | None -> () | Some spec -> Printers.pp_spec fmt spec) |
127 |
(Utils.fprintf_list ~sep:"@ " Printers.pp_expr_annot) m.mannot |
128 |
|
129 |
let pp_machines fmt ml = |
130 |
Format.fprintf fmt "@[<v 0>%a@]" (Utils.fprintf_list ~sep:"@," pp_machine) ml |
131 |
|
132 |
|
133 |
let rec is_const_value v = |
134 |
match v.value_desc with |
135 |
| Cst _ -> true |
136 |
| Fun (id, args) -> Basic_library.is_value_internal_fun v && List.for_all is_const_value args |
137 |
| _ -> false |
138 |
|
139 |
(* Returns the declared stateless status and the computed one. *) |
140 |
let get_stateless_status m = |
141 |
(m.mname.node_dec_stateless, Utils.desome m.mname.node_stateless) |
142 |
|
143 |
let is_input m id = |
144 |
List.exists (fun o -> o.var_id = id.var_id) m.mstep.step_inputs |
145 |
|
146 |
let is_output m id = |
147 |
List.exists (fun o -> o.var_id = id.var_id) m.mstep.step_outputs |
148 |
|
149 |
let is_memory m id = |
150 |
List.exists (fun o -> o.var_id = id.var_id) m.mmemory |
151 |
|
152 |
let conditional (* TODO ?(lustre_expr:expr option=None) *) c t e = |
153 |
mkinstr (* TODO ?lustre_expr *) (MBranch(c, [ (tag_true, t); (tag_false, e) ])) |
154 |
|
155 |
let dummy_var_decl name typ = |
156 |
{ |
157 |
var_id = name; |
158 |
var_orig = false; |
159 |
var_dec_type = dummy_type_dec; |
160 |
var_dec_clock = dummy_clock_dec; |
161 |
var_dec_const = false; |
162 |
var_dec_value = None; |
163 |
var_type = typ; |
164 |
var_clock = Clocks.new_ck Clocks.Cvar true; |
165 |
var_loc = Location.dummy_loc |
166 |
} |
167 |
|
168 |
let arrow_id = "_arrow" |
169 |
|
170 |
let arrow_typ = Types.new_ty Types.Tunivar |
171 |
|
172 |
let arrow_desc = |
173 |
{ |
174 |
node_id = arrow_id; |
175 |
node_type = Type_predef.type_bin_poly_op; |
176 |
node_clock = Clock_predef.ck_bin_univ; |
177 |
node_inputs= [dummy_var_decl "_in1" arrow_typ; dummy_var_decl "_in2" arrow_typ]; |
178 |
node_outputs= [dummy_var_decl "_out" arrow_typ]; |
179 |
node_locals= []; |
180 |
node_gencalls = []; |
181 |
node_checks = []; |
182 |
node_asserts = []; |
183 |
node_stmts= []; |
184 |
node_dec_stateless = false; |
185 |
node_stateless = Some false; |
186 |
node_spec = None; |
187 |
node_annot = []; } |
188 |
|
189 |
let arrow_top_decl = |
190 |
{ |
191 |
top_decl_desc = Node arrow_desc; |
192 |
top_decl_owner = (Options.core_dependency "arrow"); |
193 |
top_decl_itf = false; |
194 |
top_decl_loc = Location.dummy_loc |
195 |
} |
196 |
|
197 |
let mk_val v t = { value_desc = v; |
198 |
value_type = t; |
199 |
value_annot = None } |
200 |
|
201 |
let arrow_machine = |
202 |
let state = "_first" in |
203 |
let var_state = dummy_var_decl state (Types.new_ty Types.Tbool) in |
204 |
let var_input1 = List.nth arrow_desc.node_inputs 0 in |
205 |
let var_input2 = List.nth arrow_desc.node_inputs 1 in |
206 |
let var_output = List.nth arrow_desc.node_outputs 0 in |
207 |
let cst b = mk_val (Cst (const_of_bool b)) Type_predef.type_bool in |
208 |
let t_arg = Types.new_univar () in (* TODO Xavier: c'est bien la bonne def ? *) |
209 |
{ |
210 |
mname = arrow_desc; |
211 |
mmemory = [var_state]; |
212 |
mcalls = []; |
213 |
minstances = []; |
214 |
minit = [mkinstr (MStateAssign(var_state, cst true))]; |
215 |
mstatic = []; |
216 |
mconst = []; |
217 |
mstep = { |
218 |
step_inputs = arrow_desc.node_inputs; |
219 |
step_outputs = arrow_desc.node_outputs; |
220 |
step_locals = []; |
221 |
step_checks = []; |
222 |
step_instrs = [conditional (mk_val (StateVar var_state) Type_predef.type_bool) |
223 |
(List.map mkinstr |
224 |
[MStateAssign(var_state, cst false); |
225 |
MLocalAssign(var_output, mk_val (LocalVar var_input1) t_arg)]) |
226 |
(List.map mkinstr |
227 |
[MLocalAssign(var_output, mk_val (LocalVar var_input2) t_arg)]) ]; |
228 |
step_asserts = []; |
229 |
}; |
230 |
mspec = None; |
231 |
mannot = []; |
232 |
} |
233 |
|
234 |
let empty_desc = |
235 |
{ |
236 |
node_id = arrow_id; |
237 |
node_type = Types.bottom; |
238 |
node_clock = Clocks.bottom; |
239 |
node_inputs= []; |
240 |
node_outputs= []; |
241 |
node_locals= []; |
242 |
node_gencalls = []; |
243 |
node_checks = []; |
244 |
node_asserts = []; |
245 |
node_stmts= []; |
246 |
node_dec_stateless = true; |
247 |
node_stateless = Some true; |
248 |
node_spec = None; |
249 |
node_annot = []; } |
250 |
|
251 |
let empty_machine = |
252 |
{ |
253 |
mname = empty_desc; |
254 |
mmemory = []; |
255 |
mcalls = []; |
256 |
minstances = []; |
257 |
minit = []; |
258 |
mstatic = []; |
259 |
mconst = []; |
260 |
mstep = { |
261 |
step_inputs = []; |
262 |
step_outputs = []; |
263 |
step_locals = []; |
264 |
step_checks = []; |
265 |
step_instrs = []; |
266 |
step_asserts = []; |
267 |
}; |
268 |
mspec = None; |
269 |
mannot = []; |
270 |
} |
271 |
|
272 |
let new_instance = |
273 |
let cpt = ref (-1) in |
274 |
fun caller callee tag -> |
275 |
begin |
276 |
let o = |
277 |
if Stateless.check_node callee then |
278 |
node_name callee |
279 |
else |
280 |
Printf.sprintf "ni_%d" (incr cpt; !cpt) in |
281 |
let o = |
282 |
if !Options.ansi && is_generic_node callee |
283 |
then Printf.sprintf "%s_inst_%d" o (Utils.position (fun e -> e.expr_tag = tag) caller.node_gencalls) |
284 |
else o in |
285 |
o |
286 |
end |
287 |
|
288 |
|
289 |
(* translate_<foo> : node -> context -> <foo> -> machine code/expression *) |
290 |
(* the context contains m : state aka memory variables *) |
291 |
(* si : initialization instructions *) |
292 |
(* j : node aka machine instances *) |
293 |
(* d : local variables *) |
294 |
(* s : step instructions *) |
295 |
let translate_ident node (m, si, j, d, s) id = |
296 |
try (* id is a node var *) |
297 |
let var_id = get_node_var id node in |
298 |
if ISet.exists (fun v -> v.var_id = id) m |
299 |
then mk_val (StateVar var_id) var_id.var_type |
300 |
else mk_val (LocalVar var_id) var_id.var_type |
301 |
with Not_found -> |
302 |
try (* id is a constant *) |
303 |
let vdecl = (Corelang.var_decl_of_const (const_of_top (Hashtbl.find Corelang.consts_table id))) in |
304 |
mk_val (LocalVar vdecl) vdecl.var_type |
305 |
with Not_found -> |
306 |
(* id is a tag *) |
307 |
(* DONE construire une liste des enum declarés et alors chercher dedans la liste |
308 |
qui contient id *) |
309 |
try |
310 |
let typ = (typedef_of_top (Hashtbl.find Corelang.tag_table id)).tydef_id in |
311 |
mk_val (Cst (Const_tag id)) (Type_predef.type_const typ) |
312 |
with Not_found -> (Format.eprintf "internal error: Machine_code.translate_ident %s" id; |
313 |
assert false) |
314 |
|
315 |
let rec control_on_clock node ((m, si, j, d, s) as args) ck inst = |
316 |
match (Clocks.repr ck).cdesc with |
317 |
| Con (ck1, cr, l) -> |
318 |
let id = Clocks.const_of_carrier cr in |
319 |
control_on_clock node args ck1 (mkinstr |
320 |
(* TODO il faudrait prendre le lustre |
321 |
associé à instr et rajouter print_ck_suffix |
322 |
ck) de clocks.ml *) |
323 |
(MBranch (translate_ident node args id, |
324 |
[l, [inst]] ))) |
325 |
| _ -> inst |
326 |
|
327 |
let rec join_branches hl1 hl2 = |
328 |
match hl1, hl2 with |
329 |
| [] , _ -> hl2 |
330 |
| _ , [] -> hl1 |
331 |
| (t1, h1)::q1, (t2, h2)::q2 -> |
332 |
if t1 < t2 then (t1, h1) :: join_branches q1 hl2 else |
333 |
if t1 > t2 then (t2, h2) :: join_branches hl1 q2 |
334 |
else (t1, List.fold_right join_guards h1 h2) :: join_branches q1 q2 |
335 |
|
336 |
and join_guards inst1 insts2 = |
337 |
match get_instr_desc inst1, List.map get_instr_desc insts2 with |
338 |
| _ , [] -> |
339 |
[inst1] |
340 |
| MBranch (x1, hl1), MBranch (x2, hl2) :: q when x1 = x2 -> |
341 |
mkinstr |
342 |
(* TODO on pourrait uniquement concatener les lustres de inst1 et hd(inst2) *) |
343 |
(MBranch (x1, join_branches (sort_handlers hl1) (sort_handlers hl2))) |
344 |
:: (List.tl insts2) |
345 |
| _ -> inst1 :: insts2 |
346 |
|
347 |
let join_guards_list insts = |
348 |
List.fold_right join_guards insts [] |
349 |
|
350 |
(* specialize predefined (polymorphic) operators |
351 |
wrt their instances, so that the C semantics |
352 |
is preserved *) |
353 |
let specialize_to_c expr = |
354 |
match expr.expr_desc with |
355 |
| Expr_appl (id, e, r) -> |
356 |
if List.exists (fun e -> Types.is_bool_type e.expr_type) (expr_list_of_expr e) |
357 |
then let id = |
358 |
match id with |
359 |
| "=" -> "equi" |
360 |
| "!=" -> "xor" |
361 |
| _ -> id in |
362 |
{ expr with expr_desc = Expr_appl (id, e, r) } |
363 |
else expr |
364 |
| _ -> expr |
365 |
|
366 |
let specialize_op expr = |
367 |
match !Options.output with |
368 |
| "C" -> specialize_to_c expr |
369 |
| _ -> expr |
370 |
|
371 |
let rec translate_expr node ((m, si, j, d, s) as args) expr = |
372 |
let expr = specialize_op expr in |
373 |
let value_desc = |
374 |
match expr.expr_desc with |
375 |
| Expr_const v -> Cst v |
376 |
| Expr_ident x -> (translate_ident node args x).value_desc |
377 |
| Expr_array el -> Array (List.map (translate_expr node args) el) |
378 |
| Expr_access (t, i) -> Access (translate_expr node args t, translate_expr node args (expr_of_dimension i)) |
379 |
| Expr_power (e, n) -> Power (translate_expr node args e, translate_expr node args (expr_of_dimension n)) |
380 |
| Expr_tuple _ |
381 |
| Expr_arrow _ |
382 |
| Expr_fby _ |
383 |
| Expr_pre _ -> (Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError) |
384 |
| Expr_when (e1, _, _) -> (translate_expr node args e1).value_desc |
385 |
| Expr_merge (x, _) -> raise NormalizationError |
386 |
| Expr_appl (id, e, _) when Basic_library.is_expr_internal_fun expr -> |
387 |
let nd = node_from_name id in |
388 |
Fun (node_name nd, List.map (translate_expr node args) (expr_list_of_expr e)) |
389 |
| Expr_ite (g,t,e) -> ( |
390 |
(* special treatment depending on the active backend. For horn backend, ite |
391 |
are preserved in expression. While they are removed for C or Java |
392 |
backends. *) |
393 |
match !Options.output with |
394 |
| "horn" -> |
395 |
Fun ("ite", [translate_expr node args g; translate_expr node args t; translate_expr node args e]) |
396 |
| "C" | "java" | _ -> |
397 |
(Format.eprintf "Normalization error for backend %s: %a@." |
398 |
!Options.output |
399 |
Printers.pp_expr expr; |
400 |
raise NormalizationError) |
401 |
) |
402 |
| _ -> raise NormalizationError |
403 |
in |
404 |
mk_val value_desc expr.expr_type |
405 |
|
406 |
let translate_guard node args expr = |
407 |
match expr.expr_desc with |
408 |
| Expr_ident x -> translate_ident node args x |
409 |
| _ -> (Format.eprintf "internal error: translate_guard %s %a@." node.node_id Printers.pp_expr expr;assert false) |
410 |
|
411 |
let rec translate_act node ((m, si, j, d, s) as args) (y, expr) = |
412 |
match expr.expr_desc with |
413 |
| Expr_ite (c, t, e) -> let g = translate_guard node args c in |
414 |
conditional (* TODO ?lustre_expr:(Some expr) *) g |
415 |
[translate_act node args (y, t)] |
416 |
[translate_act node args (y, e)] |
417 |
| Expr_merge (x, hl) -> mkinstr (* TODO ?lustre_expr:(Some expr) *) (MBranch (translate_ident node args x, |
418 |
List.map (fun (t, h) -> t, [translate_act node args (y, h)]) hl)) |
419 |
| _ -> mkinstr (* TODO ?lustre_expr:(Some expr) *) (MLocalAssign (y, translate_expr node args expr)) |
420 |
|
421 |
let reset_instance node args i r c = |
422 |
match r with |
423 |
| None -> [] |
424 |
| Some r -> let g = translate_guard node args r in |
425 |
[control_on_clock node args c (conditional g [mkinstr (MReset i)] [mkinstr (MNoReset i)])] |
426 |
|
427 |
let translate_eq node ((m, si, j, d, s) as args) eq = |
428 |
(* Format.eprintf "translate_eq %a with clock %a@." Printers.pp_node_eq eq Clocks.print_ck eq.eq_rhs.expr_clock; *) |
429 |
match eq.eq_lhs, eq.eq_rhs.expr_desc with |
430 |
| [x], Expr_arrow (e1, e2) -> |
431 |
let var_x = get_node_var x node in |
432 |
let o = new_instance node arrow_top_decl eq.eq_rhs.expr_tag in |
433 |
let c1 = translate_expr node args e1 in |
434 |
let c2 = translate_expr node args e2 in |
435 |
(m, |
436 |
mkinstr (MReset o) :: si, |
437 |
Utils.IMap.add o (arrow_top_decl, []) j, |
438 |
d, |
439 |
(control_on_clock node args eq.eq_rhs.expr_clock (mkinstr (* TODO ?lustre_eq:eq *) (MStep ([var_x], o, [c1;c2])))) :: s) |
440 |
| [x], Expr_pre e1 when ISet.mem (get_node_var x node) d -> |
441 |
let var_x = get_node_var x node in |
442 |
(ISet.add var_x m, |
443 |
si, |
444 |
j, |
445 |
d, |
446 |
control_on_clock node args eq.eq_rhs.expr_clock (mkinstr (* TODO ?lustre_eq:(Some eq) *) (MStateAssign (var_x, translate_expr node args e1))) :: s) |
447 |
| [x], Expr_fby (e1, e2) when ISet.mem (get_node_var x node) d -> |
448 |
let var_x = get_node_var x node in |
449 |
(ISet.add var_x m, |
450 |
mkinstr (* TODO ?lustre_eq:(Some eq) *) (MStateAssign (var_x, translate_expr node args e1)) :: si, |
451 |
j, |
452 |
d, |
453 |
control_on_clock node args eq.eq_rhs.expr_clock (mkinstr (* TODO ?lustre_eq:(Some eq) *) (MStateAssign (var_x, translate_expr node args e2))) :: s) |
454 |
|
455 |
| p , Expr_appl (f, arg, r) when not (Basic_library.is_expr_internal_fun eq.eq_rhs) -> |
456 |
let var_p = List.map (fun v -> get_node_var v node) p in |
457 |
let el = expr_list_of_expr arg in |
458 |
let vl = List.map (translate_expr node args) el in |
459 |
let node_f = node_from_name f in |
460 |
let call_f = |
461 |
node_f, |
462 |
NodeDep.filter_static_inputs (node_inputs node_f) el in |
463 |
let o = new_instance node node_f eq.eq_rhs.expr_tag in |
464 |
let env_cks = List.fold_right (fun arg cks -> arg.expr_clock :: cks) el [eq.eq_rhs.expr_clock] in |
465 |
let call_ck = Clock_calculus.compute_root_clock (Clock_predef.ck_tuple env_cks) in |
466 |
(*Clocks.new_var true in |
467 |
Clock_calculus.unify_imported_clock (Some call_ck) eq.eq_rhs.expr_clock eq.eq_rhs.expr_loc; |
468 |
Format.eprintf "call %a: %a: %a@," Printers.pp_expr eq.eq_rhs Clocks.print_ck (Clock_predef.ck_tuple env_cks) Clocks.print_ck call_ck;*) |
469 |
(m, |
470 |
(if Stateless.check_node node_f then si else mkinstr (MReset o) :: si), |
471 |
Utils.IMap.add o call_f j, |
472 |
d, |
473 |
(if Stateless.check_node node_f |
474 |
then [] |
475 |
else reset_instance node args o r call_ck) @ |
476 |
(control_on_clock node args call_ck (mkinstr (* TODO ?lustre_eq:(Some eq) *) (MStep (var_p, o, vl)))) :: s) |
477 |
(* |
478 |
(* special treatment depending on the active backend. For horn backend, x = ite (g,t,e) |
479 |
are preserved. While they are replaced as if g then x = t else x = e in C or Java |
480 |
backends. *) |
481 |
| [x], Expr_ite (c, t, e) |
482 |
when (match !Options.output with | "horn" -> true | "C" | "java" | _ -> false) |
483 |
-> |
484 |
let var_x = get_node_var x node in |
485 |
(m, |
486 |
si, |
487 |
j, |
488 |
d, |
489 |
(control_on_clock node args eq.eq_rhs.expr_clock |
490 |
(MLocalAssign (var_x, translate_expr node args eq.eq_rhs))::s) |
491 |
) |
492 |
|
493 |
*) |
494 |
| [x], _ -> ( |
495 |
let var_x = get_node_var x node in |
496 |
(m, si, j, d, |
497 |
control_on_clock |
498 |
node |
499 |
args |
500 |
eq.eq_rhs.expr_clock |
501 |
(translate_act node args (var_x, eq.eq_rhs)) :: s |
502 |
) |
503 |
) |
504 |
| _ -> |
505 |
begin |
506 |
Format.eprintf "internal error: Machine_code.translate_eq %a@?" Printers.pp_node_eq eq; |
507 |
assert false |
508 |
end |
509 |
|
510 |
let find_eq xl eqs = |
511 |
let rec aux accu eqs = |
512 |
match eqs with |
513 |
| [] -> |
514 |
begin |
515 |
Format.eprintf "Looking for variables %a in the following equations@.%a@." |
516 |
(Utils.fprintf_list ~sep:" , " (fun fmt v -> Format.fprintf fmt "%s" v)) xl |
517 |
Printers.pp_node_eqs eqs; |
518 |
assert false |
519 |
end |
520 |
| hd::tl -> |
521 |
if List.exists (fun x -> List.mem x hd.eq_lhs) xl then hd, accu@tl else aux (hd::accu) tl |
522 |
in |
523 |
aux [] eqs |
524 |
|
525 |
(* Sort the set of equations of node [nd] according |
526 |
to the computed schedule [sch] |
527 |
*) |
528 |
let sort_equations_from_schedule nd sch = |
529 |
(* Format.eprintf "%s schedule: %a@." *) |
530 |
(* nd.node_id *) |
531 |
(* (Utils.fprintf_list ~sep:" ; " Scheduling.pp_eq_schedule) sch; *) |
532 |
let split_eqs = Splitting.tuple_split_eq_list (get_node_eqs nd) in |
533 |
let eqs_rev, remainder = |
534 |
List.fold_left |
535 |
(fun (accu, node_eqs_remainder) vl -> |
536 |
if List.exists (fun eq -> List.exists (fun v -> List.mem v eq.eq_lhs) vl) accu |
537 |
then |
538 |
(accu, node_eqs_remainder) |
539 |
else |
540 |
let eq_v, remainder = find_eq vl node_eqs_remainder in |
541 |
eq_v::accu, remainder |
542 |
) |
543 |
([], split_eqs) |
544 |
sch |
545 |
in |
546 |
begin |
547 |
if List.length remainder > 0 then ( |
548 |
Format.eprintf "Equations not used are@.%a@.Full equation set is:@.%a@.@?" |
549 |
Printers.pp_node_eqs remainder |
550 |
Printers.pp_node_eqs (get_node_eqs nd); |
551 |
assert false); |
552 |
List.rev eqs_rev |
553 |
end |
554 |
|
555 |
let constant_equations nd = |
556 |
List.fold_right (fun vdecl eqs -> |
557 |
if vdecl.var_dec_const |
558 |
then |
559 |
{ eq_lhs = [vdecl.var_id]; |
560 |
eq_rhs = Utils.desome vdecl.var_dec_value; |
561 |
eq_loc = vdecl.var_loc |
562 |
} :: eqs |
563 |
else eqs) |
564 |
nd.node_locals [] |
565 |
|
566 |
let translate_eqs node args eqs = |
567 |
List.fold_right (fun eq args -> translate_eq node args eq) eqs args;; |
568 |
|
569 |
let translate_decl nd sch = |
570 |
(*Log.report ~level:1 (fun fmt -> Printers.pp_node fmt nd);*) |
571 |
|
572 |
let sorted_eqs = sort_equations_from_schedule nd sch in |
573 |
let constant_eqs = constant_equations nd in |
574 |
|
575 |
(* In case of non functional backend (eg. C), additional local variables have |
576 |
to be declared for each assert *) |
577 |
let new_locals, assert_instrs, nd_node_asserts = |
578 |
let exprl = List.map (fun assert_ -> assert_.assert_expr ) nd.node_asserts in |
579 |
if Corelang.functional_backend () then |
580 |
[], [], exprl |
581 |
else (* Each assert(e) is associated to a fresh variable v and declared as |
582 |
v=e; assert (v); *) |
583 |
let _, vars, eql, assertl = |
584 |
List.fold_left (fun (i, vars, eqlist, assertlist) expr -> |
585 |
let loc = expr.expr_loc in |
586 |
let var_id = nd.node_id ^ "_assert_" ^ string_of_int i in |
587 |
let assert_var = |
588 |
mkvar_decl |
589 |
loc |
590 |
~orig:false (* fresh var *) |
591 |
(var_id, |
592 |
mktyp loc Tydec_bool, |
593 |
mkclock loc Ckdec_any, |
594 |
false, (* not a constant *) |
595 |
None (* no default value *) |
596 |
) |
597 |
in |
598 |
assert_var.var_type <- Types.new_ty (Types.Tbool); |
599 |
let eq = mkeq loc ([var_id], expr) in |
600 |
(i+1, assert_var::vars, eq::eqlist, {expr with expr_desc = Expr_ident var_id}::assertlist) |
601 |
) (1, [], [], []) exprl |
602 |
in |
603 |
vars, eql, assertl |
604 |
in |
605 |
let locals_list = nd.node_locals @ new_locals in |
606 |
|
607 |
let nd = { nd with node_locals = locals_list } in |
608 |
let init_args = ISet.empty, [], Utils.IMap.empty, List.fold_right (fun l -> ISet.add l) locals_list ISet.empty, [] in |
609 |
(* memories, init instructions, node calls, local variables (including memories), step instrs *) |
610 |
let m0, init0, j0, locals0, s0 = translate_eqs nd init_args constant_eqs in |
611 |
assert (ISet.is_empty m0); |
612 |
assert (init0 = []); |
613 |
assert (Utils.IMap.is_empty j0); |
614 |
let m, init, j, locals, s = translate_eqs nd (m0, init0, j0, locals0, []) (assert_instrs@sorted_eqs) in |
615 |
let mmap = Utils.IMap.fold (fun i n res -> (i, n)::res) j [] in |
616 |
{ |
617 |
mname = nd; |
618 |
mmemory = ISet.elements m; |
619 |
mcalls = mmap; |
620 |
minstances = List.filter (fun (_, (n,_)) -> not (Stateless.check_node n)) mmap; |
621 |
minit = init; |
622 |
mconst = s0; |
623 |
mstatic = List.filter (fun v -> v.var_dec_const) nd.node_inputs; |
624 |
mstep = { |
625 |
step_inputs = nd.node_inputs; |
626 |
step_outputs = nd.node_outputs; |
627 |
step_locals = ISet.elements (ISet.diff locals m); |
628 |
step_checks = List.map (fun d -> d.Dimension.dim_loc, translate_expr nd init_args (expr_of_dimension d)) nd.node_checks; |
629 |
step_instrs = ( |
630 |
(* special treatment depending on the active backend. For horn backend, |
631 |
common branches are not merged while they are in C or Java |
632 |
backends. *) |
633 |
(*match !Options.output with |
634 |
| "horn" -> s |
635 |
| "C" | "java" | _ ->*) |
636 |
if !Backends.join_guards then |
637 |
join_guards_list s |
638 |
else |
639 |
s |
640 |
); |
641 |
step_asserts = List.map (translate_expr nd init_args) nd_node_asserts; |
642 |
}; |
643 |
mspec = nd.node_spec; |
644 |
mannot = nd.node_annot; |
645 |
} |
646 |
|
647 |
(** takes the global declarations and the scheduling associated to each node *) |
648 |
let translate_prog decls node_schs = |
649 |
let nodes = get_nodes decls in |
650 |
List.map |
651 |
(fun decl -> |
652 |
let node = node_of_top decl in |
653 |
let sch = (Utils.IMap.find node.node_id node_schs).Scheduling.schedule in |
654 |
translate_decl node sch |
655 |
) nodes |
656 |
|
657 |
let get_machine_opt name machines = |
658 |
List.fold_left |
659 |
(fun res m -> |
660 |
match res with |
661 |
| Some _ -> res |
662 |
| None -> if m.mname.node_id = name then Some m else None) |
663 |
None machines |
664 |
|
665 |
let get_const_assign m id = |
666 |
try |
667 |
match get_instr_desc (List.find |
668 |
(fun instr -> match get_instr_desc instr with |
669 |
| MLocalAssign (v, _) -> v == id |
670 |
| _ -> false) |
671 |
m.mconst |
672 |
) with |
673 |
| MLocalAssign (_, e) -> e |
674 |
| _ -> assert false |
675 |
with Not_found -> assert false |
676 |
|
677 |
|
678 |
let value_of_ident loc m id = |
679 |
(* is is a state var *) |
680 |
try |
681 |
let v = List.find (fun v -> v.var_id = id) m.mmemory |
682 |
in mk_val (StateVar v) v.var_type |
683 |
with Not_found -> |
684 |
try (* id is a node var *) |
685 |
let v = get_node_var id m.mname |
686 |
in mk_val (LocalVar v) v.var_type |
687 |
with Not_found -> |
688 |
try (* id is a constant *) |
689 |
let c = Corelang.var_decl_of_const (const_of_top (Hashtbl.find Corelang.consts_table id)) |
690 |
in mk_val (LocalVar c) c.var_type |
691 |
with Not_found -> |
692 |
(* id is a tag *) |
693 |
let t = Const_tag id |
694 |
in mk_val (Cst t) (Typing.type_const loc t) |
695 |
|
696 |
(* type of internal fun used in dimension expression *) |
697 |
let type_of_value_appl f args = |
698 |
if List.mem f Basic_library.arith_funs |
699 |
then (List.hd args).value_type |
700 |
else Type_predef.type_bool |
701 |
|
702 |
let rec value_of_dimension m dim = |
703 |
match dim.Dimension.dim_desc with |
704 |
| Dimension.Dbool b -> |
705 |
mk_val (Cst (Const_tag (if b then Corelang.tag_true else Corelang.tag_false))) Type_predef.type_bool |
706 |
| Dimension.Dint i -> |
707 |
mk_val (Cst (Const_int i)) Type_predef.type_int |
708 |
| Dimension.Dident v -> value_of_ident dim.Dimension.dim_loc m v |
709 |
| Dimension.Dappl (f, args) -> |
710 |
let vargs = List.map (value_of_dimension m) args |
711 |
in mk_val (Fun (f, vargs)) (type_of_value_appl f vargs) |
712 |
| Dimension.Dite (i, t, e) -> |
713 |
(match List.map (value_of_dimension m) [i; t; e] with |
714 |
| [vi; vt; ve] -> mk_val (Fun ("ite", [vi; vt; ve])) vt.value_type |
715 |
| _ -> assert false) |
716 |
| Dimension.Dlink dim' -> value_of_dimension m dim' |
717 |
| _ -> assert false |
718 |
|
719 |
let rec dimension_of_value value = |
720 |
match value.value_desc with |
721 |
| Cst (Const_tag t) when t = Corelang.tag_true -> Dimension.mkdim_bool Location.dummy_loc true |
722 |
| Cst (Const_tag t) when t = Corelang.tag_false -> Dimension.mkdim_bool Location.dummy_loc false |
723 |
| Cst (Const_int i) -> Dimension.mkdim_int Location.dummy_loc i |
724 |
| LocalVar v -> Dimension.mkdim_ident Location.dummy_loc v.var_id |
725 |
| Fun (f, args) -> Dimension.mkdim_appl Location.dummy_loc f (List.map dimension_of_value args) |
726 |
| _ -> assert false |
727 |
|
728 |
(* Local Variables: *) |
729 |
(* compile-command:"make -C .." *) |
730 |
(* End: *) |