lustrec / src / machine_code.ml @ 7c95dcab
History  View  Annotate  Download (22.6 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 
exception NormalizationError 
18  
19 
module OrdVarDecl:Map.OrderedType with type t=var_decl = 
20 
struct type t = var_decl;; let compare = compare end 
21  
22 
module ISet = Set.Make(OrdVarDecl) 
23  
24 
type value_t = 
25 
 Cst of constant 
26 
 LocalVar of var_decl 
27 
 StateVar of var_decl 
28 
 Fun of ident * value_t list 
29 
 Array of value_t list 
30 
 Access of value_t * value_t 
31 
 Power of value_t * value_t 
32  
33 
type instr_t = 
34 
 MLocalAssign of var_decl * value_t 
35 
 MStateAssign of var_decl * value_t 
36 
 MReset of ident 
37 
 MStep of var_decl list * ident * value_t list 
38 
 MBranch of value_t * (label * instr_t list) list 
39  
40 
let rec pp_val fmt v = 
41 
match v with 
42 
 Cst c > Printers.pp_const fmt c 
43 
 LocalVar v > Format.pp_print_string fmt v.var_id 
44 
 StateVar v > Format.pp_print_string fmt v.var_id 
45 
 Array vl > Format.fprintf fmt "[%a]" (Utils.fprintf_list ~sep:", " pp_val) vl 
46 
 Access (t, i) > Format.fprintf fmt "%a[%a]" pp_val t pp_val i 
47 
 Power (v, n) > Format.fprintf fmt "(%a^%a)" pp_val v pp_val n 
48 
 Fun (n, vl) > Format.fprintf fmt "%s (%a)" n (Utils.fprintf_list ~sep:", " pp_val) vl 
49  
50 
let rec pp_instr fmt i = 
51 
match i with 
52 
 MLocalAssign (i,v) > Format.fprintf fmt "%s<l %a" i.var_id pp_val v 
53 
 MStateAssign (i,v) > Format.fprintf fmt "%s<s %a" i.var_id pp_val v 
54 
 MReset i > Format.fprintf fmt "reset %s" i 
55 
 MStep (il, i, vl) > 
56 
Format.fprintf fmt "%a = %s (%a)" 
57 
(Utils.fprintf_list ~sep:", " (fun fmt v > Format.pp_print_string fmt v.var_id)) il 
58 
i 
59 
(Utils.fprintf_list ~sep:", " pp_val) vl 
60 
 MBranch (g,hl) > 
61 
Format.fprintf fmt "@[<v 2>case(%a) {@,%a@,}@]" 
62 
pp_val g 
63 
(Utils.fprintf_list ~sep:"@," pp_branch) hl 
64  
65 
and pp_branch fmt (t, h) = 
66 
Format.fprintf fmt "@[<v 2>%s:@,%a@]" t (Utils.fprintf_list ~sep:"@," pp_instr) h 
67  
68 
and pp_instrs fmt il = 
69 
Format.fprintf fmt "@[<v 2>%a@]" (Utils.fprintf_list ~sep:"@," pp_instr) il 
70  
71 
type step_t = { 
72 
step_checks: (Location.t * value_t) list; 
73 
step_inputs: var_decl list; 
74 
step_outputs: var_decl list; 
75 
step_locals: var_decl list; 
76 
step_instrs: instr_t list; 
77 
step_asserts: value_t list; 
78 
} 
79  
80 
type static_call = top_decl * (Dimension.dim_expr list) 
81  
82 
type machine_t = { 
83 
mname: node_desc; 
84 
mmemory: var_decl list; 
85 
mcalls: (ident * static_call) list; (* map from stateful/stateless instance to node, no internals *) 
86 
minstances: (ident * static_call) list; (* submap of mcalls, from stateful instance to node *) 
87 
minit: instr_t list; 
88 
mstatic: var_decl list; (* static inputs only *) 
89 
mconst: instr_t list; (* assignments of node constant locals *) 
90 
mstep: step_t; 
91 
mspec: node_annot option; 
92 
mannot: expr_annot list; 
93 
} 
94  
95 
let pp_step fmt s = 
96 
Format.fprintf fmt "@[<v>inputs : %a@ outputs: %a@ locals : %a@ checks : %a@ instrs : @[%a@]@ asserts : @[%a@]@]@ " 
97 
(Utils.fprintf_list ~sep:", " Printers.pp_var) s.step_inputs 
98 
(Utils.fprintf_list ~sep:", " Printers.pp_var) s.step_outputs 
99 
(Utils.fprintf_list ~sep:", " Printers.pp_var) s.step_locals 
100 
(Utils.fprintf_list ~sep:", " (fun fmt (_, c) > pp_val fmt c)) s.step_checks 
101 
(Utils.fprintf_list ~sep:"@ " pp_instr) s.step_instrs 
102 
(Utils.fprintf_list ~sep:", " pp_val) s.step_asserts 
103  
104  
105 
let pp_static_call fmt (node, args) = 
106 
Format.fprintf fmt "%s<%a>" 
107 
(node_name node) 
108 
(Utils.fprintf_list ~sep:", " Dimension.pp_dimension) args 
109  
110 
let pp_machine fmt m = 
111 
Format.fprintf fmt 
112 
"@[<v 2>machine %s@ mem : %a@ instances: %a@ init : %a@ const : %a@ step :@ @[<v 2>%a@]@ @ spec : @[%t@]@ annot : @[%a@]@]@ " 
113 
m.mname.node_id 
114 
(Utils.fprintf_list ~sep:", " Printers.pp_var) m.mmemory 
115 
(Utils.fprintf_list ~sep:", " (fun fmt (o1, o2) > Format.fprintf fmt "(%s, %a)" o1 pp_static_call o2)) m.minstances 
116 
(Utils.fprintf_list ~sep:"@ " pp_instr) m.minit 
117 
(Utils.fprintf_list ~sep:"@ " pp_instr) m.mconst 
118 
pp_step m.mstep 
119 
(fun fmt > match m.mspec with  None > ()  Some spec > Printers.pp_spec fmt spec) 
120 
(Utils.fprintf_list ~sep:"@ " Printers.pp_expr_annot) m.mannot 
121  
122 
(* Returns the declared stateless status and the computed one. *) 
123 
let get_stateless_status m = 
124 
(m.mname.node_dec_stateless, Utils.desome m.mname.node_stateless) 
125  
126 
let is_input m id = 
127 
List.exists (fun o > o.var_id = id.var_id) m.mstep.step_inputs 
128  
129 
let is_output m id = 
130 
List.exists (fun o > o.var_id = id.var_id) m.mstep.step_outputs 
131  
132 
let is_memory m id = 
133 
List.exists (fun o > o.var_id = id.var_id) m.mmemory 
134  
135 
let conditional c t e = 
136 
MBranch(c, [ (tag_true, t); (tag_false, e) ]) 
137  
138 
let dummy_var_decl name typ = 
139 
{ 
140 
var_id = name; 
141 
var_orig = false; 
142 
var_dec_type = dummy_type_dec; 
143 
var_dec_clock = dummy_clock_dec; 
144 
var_dec_const = false; 
145 
var_dec_value = None; 
146 
var_type = typ; 
147 
var_clock = Clocks.new_ck (Clocks.Cvar Clocks.CSet_all) true; 
148 
var_loc = Location.dummy_loc 
149 
} 
150  
151 
let arrow_id = "_arrow" 
152  
153 
let arrow_typ = Types.new_ty Types.Tunivar 
154  
155 
let arrow_desc = 
156 
{ 
157 
node_id = arrow_id; 
158 
node_type = Type_predef.type_bin_poly_op; 
159 
node_clock = Clock_predef.ck_bin_univ; 
160 
node_inputs= [dummy_var_decl "_in1" arrow_typ; dummy_var_decl "_in2" arrow_typ]; 
161 
node_outputs= [dummy_var_decl "_out" arrow_typ]; 
162 
node_locals= []; 
163 
node_gencalls = []; 
164 
node_checks = []; 
165 
node_asserts = []; 
166 
node_stmts= []; 
167 
node_dec_stateless = false; 
168 
node_stateless = Some false; 
169 
node_spec = None; 
170 
node_annot = []; } 
171  
172 
let arrow_top_decl = 
173 
{ 
174 
top_decl_desc = Node arrow_desc; 
175 
top_decl_owner = Version.include_path; 
176 
top_decl_itf = false; 
177 
top_decl_loc = Location.dummy_loc 
178 
} 
179  
180 
let arrow_machine = 
181 
let state = "_first" in 
182 
let var_state = dummy_var_decl state (Types.new_ty Types.Tbool) in 
183 
let var_input1 = List.nth arrow_desc.node_inputs 0 in 
184 
let var_input2 = List.nth arrow_desc.node_inputs 1 in 
185 
let var_output = List.nth arrow_desc.node_outputs 0 in 
186 
{ 
187 
mname = arrow_desc; 
188 
mmemory = [var_state]; 
189 
mcalls = []; 
190 
minstances = []; 
191 
minit = [MStateAssign(var_state, Cst (const_of_bool true))]; 
192 
mconst = []; 
193 
mstatic = []; 
194 
mstep = { 
195 
step_inputs = arrow_desc.node_inputs; 
196 
step_outputs = arrow_desc.node_outputs; 
197 
step_locals = []; 
198 
step_checks = []; 
199 
step_instrs = [conditional (StateVar var_state) 
200 
[MStateAssign(var_state, Cst (const_of_bool false)); 
201 
MLocalAssign(var_output, LocalVar var_input1)] 
202 
[MLocalAssign(var_output, LocalVar var_input2)] ]; 
203 
step_asserts = []; 
204 
}; 
205 
mspec = None; 
206 
mannot = []; 
207 
} 
208  
209 
let new_instance = 
210 
let cpt = ref (1) in 
211 
fun caller callee tag > 
212 
begin 
213 
let o = 
214 
if Stateless.check_node callee then 
215 
node_name callee 
216 
else 
217 
Printf.sprintf "ni_%d" (incr cpt; !cpt) in 
218 
let o = 
219 
if !Options.ansi && is_generic_node callee 
220 
then Printf.sprintf "%s_inst_%d" o (Utils.position (fun e > e.expr_tag = tag) caller.node_gencalls) 
221 
else o in 
222 
o 
223 
end 
224  
225  
226 
(* translate_<foo> : node > context > <foo> > machine code/expression *) 
227 
(* the context contains m : state aka memory variables *) 
228 
(* si : initialization instructions *) 
229 
(* j : node aka machine instances *) 
230 
(* d : local variables *) 
231 
(* s : step instructions *) 
232 
let translate_ident node (m, si, j, d, s) id = 
233 
try (* id is a node var *) 
234 
let var_id = get_node_var id node in 
235 
if ISet.exists (fun v > v.var_id = id) m 
236 
then StateVar var_id 
237 
else LocalVar var_id 
238 
with Not_found > 
239 
try (* id is a constant *) 
240 
LocalVar (Corelang.var_decl_of_const (const_of_top (Hashtbl.find Corelang.consts_table id))) 
241 
with Not_found > 
242 
(* id is a tag *) 
243 
Cst (Const_tag 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 
(* specialize predefined (polymorphic) operators 
275 
wrt their instances, so that the C semantics 
276 
is preserved *) 
277 
let specialize_to_c expr = 
278 
match expr.expr_desc with 
279 
 Expr_appl (id, e, r) > 
280 
if List.exists (fun e > Types.is_bool_type e.expr_type) (expr_list_of_expr e) 
281 
then let id = 
282 
match id with 
283 
 "=" > "equi" 
284 
 "!=" > "xor" 
285 
 _ > id in 
286 
{ expr with expr_desc = Expr_appl (id, e, r) } 
287 
else expr 
288 
 _ > expr 
289  
290 
let specialize_op expr = 
291 
match !Options.output with 
292 
 "C" > specialize_to_c expr 
293 
 _ > expr 
294  
295 
let rec merge_to_ite g hl = 
296 
let loc = Location.dummy_loc in 
297 
let mkcst x = mkexpr loc (Expr_const (Const_tag x)) in 
298 
let g_expr = mkcst g in 
299 
match hl with 
300 
 [] > assert false 
301 
 [_, e] > e 
302 
 (l_c,l_e)::tl > 
303 
let cond_expr = 
304 
mkpredef_call loc "=" [g_expr; mkcst l_c] 
305 
in 
306 
mkexpr loc (Expr_ite (cond_expr, l_e, merge_to_ite g tl)) 
307 

308 
let rec translate_expr ?(ite=false) node ((m, si, j, d, s) as args) expr = 
309 
let expr = specialize_op expr in 
310 
match expr.expr_desc with 
311 
 Expr_const v > Cst v 
312 
 Expr_ident x > translate_ident node args x 
313 
 Expr_array el > Array (List.map (translate_expr node args) el) 
314 
 Expr_access (t, i) > Access (translate_expr node args t, translate_expr node args (expr_of_dimension i)) 
315 
 Expr_power (e, n) > Power (translate_expr node args e, translate_expr node args (expr_of_dimension n)) 
316 
 Expr_tuple _ 
317 
 Expr_arrow _ 
318 
 Expr_fby _ 
319 
 Expr_pre _ > (Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError) 
320 
 Expr_when (e1, _, _) > translate_expr node args e1 
321 
 Expr_merge (g, hl) > ( 
322 
(* Special treatment for functional backends. Is transformed into Ite *) 
323 
match !Options.output with 
324 
 "horn" > translate_expr node args (merge_to_ite g hl) 
325 
 ("C"  "java") > raise NormalizationError (* should have been replaced by MBranch *) 
326 
 _ > 
327 
(Format.eprintf "option:%s@." !Options.output; Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError) 
328  
329 
) 
330 

331 
 Expr_appl (id, e, _) when Basic_library.is_internal_fun id > 
332 
let nd = node_from_name id in 
333 
Fun (node_name nd, List.map (translate_expr node args) (expr_list_of_expr e)) 
334 
 Expr_ite (g,t,e) > ( 
335 
(* special treatment depending on the active backend. For horn backend, ite 
336 
are preserved in expression. While they are removed for C or Java 
337 
backends. *) 
338 
match !Options.output with 
339 
 "horn" > 
340 
Fun ("ite", [translate_expr node args g; translate_expr node args t; translate_expr node args e]) 
341 
 ("C"  "java") when ite > 
342 
Fun ("ite", [translate_expr node args g; translate_expr node args t; translate_expr node args e]) 
343 
 _ > 
344 
(Format.eprintf "option:%s@." !Options.output; Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError) 
345 
) 
346 
 _ > raise NormalizationError 
347  
348 
let translate_guard node args expr = 
349 
match expr.expr_desc with 
350 
 Expr_ident x > translate_ident node args x 
351 
 _ > (Format.eprintf "internal error: translate_guard %s %a@." node.node_id Printers.pp_expr expr;assert false) 
352  
353 
let rec translate_act node ((m, si, j, d, s) as args) (y, expr) = 
354 
match expr.expr_desc with 
355 
 Expr_ite (c, t, e) > let g = translate_guard node args c in 
356 
conditional g [translate_act node args (y, t)] 
357 
[translate_act node args (y, e)] 
358 
 Expr_merge (x, hl) > MBranch (translate_ident node args x, List.map (fun (t, h) > t, [translate_act node args (y, h)]) hl) 
359 
 _ > 
360 
MLocalAssign (y, translate_expr node args expr) 
361  
362 
let reset_instance node args i r c = 
363 
match r with 
364 
 None > [] 
365 
 Some r > let g = translate_guard node args r in 
366 
[control_on_clock node args c (conditional g [MReset i] [])] 
367  
368 
let translate_eq node ((m, si, j, d, s) as args) eq = 
369 
(* Format.eprintf "translate_eq %a with clock %a@." Printers.pp_node_eq eq Clocks.print_ck eq.eq_rhs.expr_clock; *) 
370 
match eq.eq_lhs, eq.eq_rhs.expr_desc with 
371 
 [x], Expr_arrow (e1, e2) > 
372 
let var_x = get_node_var x node in 
373 
let o = new_instance node arrow_top_decl eq.eq_rhs.expr_tag in 
374 
let c1 = translate_expr node args e1 in 
375 
let c2 = translate_expr node args e2 in 
376 
(m, 
377 
MReset o :: si, 
378 
Utils.IMap.add o (arrow_top_decl, []) j, 
379 
d, 
380 
(control_on_clock node args eq.eq_rhs.expr_clock (MStep ([var_x], o, [c1;c2]))) :: s) 
381 
 [x], Expr_pre e1 when ISet.mem (get_node_var x node) d > 
382 
let var_x = get_node_var x node in 
383 
(ISet.add var_x m, 
384 
si, 
385 
j, 
386 
d, 
387 
control_on_clock node args eq.eq_rhs.expr_clock (MStateAssign (var_x, translate_expr node args e1)) :: s) 
388 
 [x], Expr_fby (e1, e2) when ISet.mem (get_node_var x node) d > 
389 
let var_x = get_node_var x node in 
390 
(ISet.add var_x m, 
391 
MStateAssign (var_x, translate_expr node args e1) :: si, 
392 
j, 
393 
d, 
394 
control_on_clock node args eq.eq_rhs.expr_clock (MStateAssign (var_x, translate_expr node args e2)) :: s) 
395  
396 
 p , Expr_appl (f, arg, r) when not (Basic_library.is_internal_fun f) > 
397 
let var_p = List.map (fun v > get_node_var v node) p in 
398 
let el = expr_list_of_expr arg in 
399 
let vl = List.map (translate_expr node args) el in 
400 
let node_f = node_from_name f in 
401 
let call_f = 
402 
node_f, 
403 
NodeDep.filter_static_inputs (node_inputs node_f) el in 
404 
let o = new_instance node node_f eq.eq_rhs.expr_tag in 
405 
let env_cks = List.fold_right (fun arg cks > arg.expr_clock :: cks) el [eq.eq_rhs.expr_clock] in 
406 
let call_ck = Clock_calculus.compute_root_clock (Clock_predef.ck_tuple env_cks) in 
407 
(*Clocks.new_var true in 
408 
Clock_calculus.unify_imported_clock (Some call_ck) eq.eq_rhs.expr_clock eq.eq_rhs.expr_loc; 
409 
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;*) 
410 
(m, 
411 
(if Stateless.check_node node_f then si else MReset o :: si), 
412 
Utils.IMap.add o call_f j, 
413 
d, 
414 
(if Stateless.check_node node_f 
415 
then [] 
416 
else reset_instance node args o r call_ck) @ 
417 
(control_on_clock node args call_ck (MStep (var_p, o, vl))) :: s) 
418  
419 
(* special treatment depending on the active backend. For horn backend, x = ite (g,t,e) 
420 
are preserved. While they are replaced as if g then x = t else x = e in C or Java 
421 
backends. *) 
422 
 [x], Expr_ite _ 
423 
(* similar treatment for merge, avoid generating MBranch instructions when using Horn backend *) 
424 
 [x], Expr_merge _ 
425 
when (match !Options.output with  "horn" > true  "C"  "java"  _ > false) 
426  
427 
(* Remark for Ocaml: the when is shared among the two patterns *) 
428 
> 
429 
let var_x = get_node_var x node in 
430 
(m, 
431 
si, 
432 
j, 
433 
d, 
434 
(control_on_clock node args eq.eq_rhs.expr_clock 
435 
(MLocalAssign (var_x, translate_expr node args eq.eq_rhs))::s) 
436 
) 
437  
438 

439 
 [x], _ > ( 
440 
let var_x = get_node_var x node in 
441 
(m, si, j, d, 
442 
control_on_clock 
443 
node 
444 
args 
445 
eq.eq_rhs.expr_clock 
446 
(translate_act node args (var_x, eq.eq_rhs)) :: s 
447 
) 
448 
) 
449 
 _ > 
450 
begin 
451 
Format.eprintf "unsupported equation: %a@?" Printers.pp_node_eq eq; 
452 
assert false 
453 
end 
454  
455 
let find_eq xl eqs = 
456 
let rec aux accu eqs = 
457 
match eqs with 
458 
 [] > 
459 
begin 
460 
Format.eprintf "Looking for variables %a in the following equations@.%a@." 
461 
(Utils.fprintf_list ~sep:" , " (fun fmt v > Format.fprintf fmt "%s" v)) xl 
462 
Printers.pp_node_eqs eqs; 
463 
assert false 
464 
end 
465 
 hd::tl > 
466 
if List.exists (fun x > List.mem x hd.eq_lhs) xl then hd, accu@tl else aux (hd::accu) tl 
467 
in 
468 
aux [] eqs 
469  
470 
(* Sort the set of equations of node [nd] according 
471 
to the computed schedule [sch] 
472 
*) 
473 
let sort_equations_from_schedule nd sch = 
474 
(*Format.eprintf "%s schedule: %a@." 
475 
nd.node_id 
476 
(Utils.fprintf_list ~sep:" ; " Scheduling.pp_eq_schedule) sch;*) 
477 
let split_eqs = Splitting.tuple_split_eq_list (get_node_eqs nd) in 
478 
let eqs_rev, remainder = 
479 
List.fold_left 
480 
(fun (accu, node_eqs_remainder) vl > 
481 
if List.exists (fun eq > List.exists (fun v > List.mem v eq.eq_lhs) vl) accu 
482 
then 
483 
(accu, node_eqs_remainder) 
484 
else 
485 
let eq_v, remainder = find_eq vl node_eqs_remainder in 
486 
eq_v::accu, remainder 
487 
) 
488 
([], split_eqs) 
489 
sch 
490 
in 
491 
begin 
492 
if List.length remainder > 0 then ( 
493 
Format.eprintf "Equations not used are@.%a@.Full equation set is:@.%a@.@?" 
494 
Printers.pp_node_eqs remainder 
495 
Printers.pp_node_eqs (get_node_eqs nd); 
496 
assert false); 
497 
List.rev eqs_rev 
498 
end 
499  
500 
let constant_equations nd = 
501 
List.fold_right (fun vdecl eqs > 
502 
if vdecl.var_dec_const 
503 
then 
504 
{ eq_lhs = [vdecl.var_id]; 
505 
eq_rhs = Utils.desome vdecl.var_dec_value; 
506 
eq_loc = vdecl.var_loc 
507 
} :: eqs 
508 
else eqs) 
509 
nd.node_locals [] 
510  
511 
let translate_eqs node args eqs = 
512 
List.fold_right (fun eq args > translate_eq node args eq) eqs args;; 
513  
514 
let translate_decl nd sch = 
515 
(*Log.report ~level:1 (fun fmt > Printers.pp_node fmt nd);*) 
516  
517 
let sorted_eqs = sort_equations_from_schedule nd sch in 
518 
let constant_eqs = constant_equations nd in 
519 

520 
let init_args = ISet.empty, [], Utils.IMap.empty, List.fold_right (fun l > ISet.add l) nd.node_locals ISet.empty, [] in 
521 
(* memories, init instructions, node calls, local variables (including memories), step instrs *) 
522 
let m0, init0, j0, locals0, s0 = translate_eqs nd init_args constant_eqs in 
523 
assert (ISet.is_empty m0); 
524 
assert (init0 = []); 
525 
assert (Utils.IMap.is_empty j0); 
526 
let m, init, j, locals, s = translate_eqs nd (m0, init0, j0, locals0, s0) sorted_eqs in 
527 
let mmap = Utils.IMap.fold (fun i n res > (i, n)::res) j [] in 
528 
{ 
529 
mname = nd; 
530 
mmemory = ISet.elements m; 
531 
mcalls = mmap; 
532 
minstances = List.filter (fun (_, (n,_)) > not (Stateless.check_node n)) mmap; 
533 
minit = init; 
534 
mconst = s0; 
535 
mstatic = List.filter (fun v > v.var_dec_const) nd.node_inputs; 
536 
mstep = { 
537 
step_inputs = nd.node_inputs; 
538 
step_outputs = nd.node_outputs; 
539 
step_locals = ISet.elements (ISet.diff locals m); 
540 
step_checks = List.map (fun d > d.Dimension.dim_loc, translate_expr nd init_args (expr_of_dimension d)) nd.node_checks; 
541 
step_instrs = ( 
542 
(* special treatment depending on the active backend. For horn backend, 
543 
common branches are not merged while they are in C or Java 
544 
backends. *) 
545 
match !Options.output with 
546 
 "horn" > s 
547 
 "C"  "java"  _ > join_guards_list s 
548 
); 
549 
step_asserts = 
550 
let exprl = List.map (fun assert_ > assert_.assert_expr ) nd.node_asserts in 
551 
List.map (translate_expr nd init_args) exprl 
552 
; 
553 
}; 
554 
mspec = nd.node_spec; 
555 
mannot = nd.node_annot; 
556 
} 
557  
558 
(** takes the global declarations and the scheduling associated to each node *) 
559 
let translate_prog decls node_schs = 
560 
let nodes = get_nodes decls in 
561 
List.map 
562 
(fun decl > 
563 
let node = node_of_top decl in 
564 
let sch = (Utils.IMap.find node.node_id node_schs).Scheduling.schedule in 
565 
translate_decl node sch 
566 
) nodes 
567  
568 
let get_machine_opt name machines = 
569 
List.fold_left 
570 
(fun res m > 
571 
match res with 
572 
 Some _ > res 
573 
 None > if m.mname.node_id = name then Some m else None) 
574 
None machines 
575  
576 
let get_const_assign m id = 
577 
try 
578 
match (List.find (fun instr > match instr with MLocalAssign (v, _) > v == id  _ > false) m.mconst) with 
579 
 MLocalAssign (_, e) > e 
580 
 _ > assert false 
581 
with Not_found > assert false 
582  
583  
584 
let value_of_ident m id = 
585 
(* is is a state var *) 
586 
try 
587 
StateVar (List.find (fun v > v.var_id = id) m.mmemory) 
588 
with Not_found > 
589 
try (* id is a node var *) 
590 
LocalVar (get_node_var id m.mname) 
591 
with Not_found > 
592 
try (* id is a constant *) 
593 
LocalVar (Corelang.var_decl_of_const (const_of_top (Hashtbl.find Corelang.consts_table id))) 
594 
with Not_found > 
595 
(* id is a tag *) 
596 
Cst (Const_tag id) 
597  
598 
let rec value_of_dimension m dim = 
599 
match dim.Dimension.dim_desc with 
600 
 Dimension.Dbool b > Cst (Const_tag (if b then Corelang.tag_true else Corelang.tag_false)) 
601 
 Dimension.Dint i > Cst (Const_int i) 
602 
 Dimension.Dident v > value_of_ident m v 
603 
 Dimension.Dappl (f, args) > Fun (f, List.map (value_of_dimension m) args) 
604 
 Dimension.Dite (i, t, e) > Fun ("ite", List.map (value_of_dimension m) [i; t; e]) 
605 
 Dimension.Dlink dim' > value_of_dimension m dim' 
606 
 _ > assert false 
607  
608 
let rec dimension_of_value value = 
609 
match value with 
610 
 Cst (Const_tag t) when t = Corelang.tag_true > Dimension.mkdim_bool Location.dummy_loc true 
611 
 Cst (Const_tag t) when t = Corelang.tag_false > Dimension.mkdim_bool Location.dummy_loc false 
612 
 Cst (Const_int i) > Dimension.mkdim_int Location.dummy_loc i 
613 
 LocalVar v > Dimension.mkdim_ident Location.dummy_loc v.var_id 
614 
 Fun (f, args) > Dimension.mkdim_appl Location.dummy_loc f (List.map dimension_of_value args) 
615 
 _ > assert false 
616  
617 
(* Local Variables: *) 
618 
(* compilecommand:"make C .." *) 
619 
(* End: *) 