lustrec / src / machine_code.ml @ df647a81
History  View  Annotate  Download (27.9 KB)
1  

2 
(*  
3 
* SchedMCore  A MultiCore Scheduling Framework 
4 
* Copyright (C) 20092013, ONERA, Toulouse, FRANCE  LIFL, Lille, FRANCE 
5 
* Copyright (C) 20122013, 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 021111307 
22 
* USA 
23 
* *) 
24  
25 
(* This module is used for the lustre to C compiler *) 
26  
27 
open Corelang 
28 
open Clocks 
29 
open Causality 
30  
31 
exception NormalizationError 
32  
33 
module OrdVarDecl:Map.OrderedType with type t=var_decl = 
34 
struct type t = var_decl;; let compare = compare end 
35  
36 
module ISet = Set.Make(OrdVarDecl) 
37  
38 
type value_t = 
39 
 Cst of constant 
40 
 LocalVar of var_decl 
41 
 StateVar of var_decl 
42 
 Fun of ident * value_t list 
43 
 Array of value_t list 
44 
 Access of value_t * value_t 
45 
 Power of value_t * value_t 
46  
47 
type instr_t = 
48 
 MLocalAssign of var_decl * value_t 
49 
 MStateAssign of var_decl * value_t 
50 
 MReset of ident 
51 
 MStep of var_decl list * ident * value_t list 
52 
 MBranch of value_t * (label * instr_t list) list 
53 

54 
let rec pp_val fmt v = 
55 
match v with 
56 
 Cst c > Printers.pp_const fmt c 
57 
 LocalVar v > Format.pp_print_string fmt v.var_id 
58 
 StateVar v > Format.pp_print_string fmt v.var_id 
59 
 Array vl > Format.fprintf fmt "[%a]" (Utils.fprintf_list ~sep:", " pp_val) vl 
60 
 Access (t, i) > Format.fprintf fmt "%a[%a]" pp_val t pp_val i 
61 
 Power (v, n) > Format.fprintf fmt "(%a^%a)" pp_val v pp_val n 
62 
 Fun (n, vl) > Format.fprintf fmt "%s (%a)" n (Utils.fprintf_list ~sep:", " pp_val) vl 
63  
64 
let rec pp_instr fmt i = 
65 
match i with 
66 
 MLocalAssign (i,v) > Format.fprintf fmt "%s<l %a" i.var_id pp_val v 
67 
 MStateAssign (i,v) > Format.fprintf fmt "%s<s %a" i.var_id pp_val v 
68 
 MReset i > Format.fprintf fmt "reset %s" i 
69 
 MStep (il, i, vl) > 
70 
Format.fprintf fmt "%a = %s (%a)" 
71 
(Utils.fprintf_list ~sep:", " (fun fmt v > Format.pp_print_string fmt v.var_id)) il 
72 
i 
73 
(Utils.fprintf_list ~sep:", " pp_val) vl 
74 
 MBranch (g,hl) > 
75 
Format.fprintf fmt "@[<v 2>case(%a) {@,%a@,}@]" 
76 
pp_val g 
77 
(Utils.fprintf_list ~sep:"@," pp_branch) hl 
78  
79 
and pp_branch fmt (t, h) = 
80 
Format.fprintf fmt "@[<v 2>%s:@,%a@]" t (Utils.fprintf_list ~sep:"@," pp_instr) h 
81  
82 
type step_t = { 
83 
step_checks: (Location.t * value_t) list; 
84 
step_inputs: var_decl list; 
85 
step_outputs: var_decl list; 
86 
step_locals: var_decl list; 
87 
step_instrs: instr_t list; 
88 
} 
89  
90 
type static_call = top_decl * (Dimension.dim_expr list) 
91  
92  
93 
type eexpr_minimachine_t = { 
94 
muid: tag; 
95 
mquantifiers: (quantifier_type * var_decl list) list; 
96 
mmmemory: var_decl list; 
97 
mmcalls: (ident * static_call) list; (* map from stateful/stateless instance to node, 
98 
no internals *) 
99 
mminstances: (ident * static_call) list; (* submap of mcalls, from stateful instance to node *) 
100 
mminit: instr_t list; 
101 
mmstep_logic: step_t; 
102 
mmstep_effects: step_t; 
103 
(* mmlogic: step_t; *) 
104 
} 
105  
106 
type spec_machine_t = { 
107 
m_requires: eexpr_minimachine_t list; 
108 
m_ensures: eexpr_minimachine_t list; 
109 
m_behaviors: (string * eexpr_minimachine_t list * eexpr_minimachine_t list) list; 
110 
} 
111  
112 
type machine_t = { 
113 
mname: node_desc; 
114 
mmemory: var_decl list; 
115 
mcalls: (ident * static_call) list; (* map from stateful/stateless instance to node, no internals *) 
116 
minstances: (ident * static_call) list; (* submap of mcalls, from stateful instance to node *) 
117 
minit: instr_t list; 
118 
mstatic: var_decl list; (* static inputs only *) 
119 
mstep: step_t; 
120 
mspec: spec_machine_t option; 
121 
mannot: (string list * eexpr_minimachine_t) list; 
122 
} 
123  
124 
let get_val_type v = 
125 
match v with 
126 
 Cst c > (Typing.type_const Location.dummy_loc c).Types.tdesc 
127 
 LocalVar v 
128 
 StateVar v> (Types.repr v.var_type).Types.tdesc 
129 
 Fun _ 
130 
 Array _ 
131 
 Access _ 
132 
 Power _ > raise (Not_found) (* Not a variable *) 
133  
134 
let pp_step fmt s = 
135 
Format.fprintf fmt "@[<v>inputs : %a@ outputs: %a@ locals : %a@ checks : %a@ instrs : @[%a@]@]@ " 
136 
(Utils.fprintf_list ~sep:", " Printers.pp_var) s.step_inputs 
137 
(Utils.fprintf_list ~sep:", " Printers.pp_var) s.step_outputs 
138 
(Utils.fprintf_list ~sep:", " Printers.pp_var) s.step_locals 
139 
(Utils.fprintf_list ~sep:", " (fun fmt (_, c) > pp_val fmt c)) s.step_checks 
140 
(Utils.fprintf_list ~sep:"@ " pp_instr) s.step_instrs 
141  
142 
let pp_static_call fmt (node, args) = 
143 
Format.fprintf fmt "%s<%a>" 
144 
(node_name node) 
145 
(Utils.fprintf_list ~sep:", " Dimension.pp_dimension) args 
146  
147 
let pp_eexpr fmt ee = 
148 
Format.fprintf fmt 
149 
"%a%t @[<v 2>mem : %a@;instances: %a@;init : %a@;logic step :@; @[<v 2>%a@]@;effects step :@; @[<v 2>%a@]@;@]@;" 
150 
(Utils.fprintf_list ~sep:"; " Printers.pp_quantifiers) ee.mquantifiers 
151 
(fun fmt > match ee.mquantifiers with [] > ()  _ > Format.fprintf fmt ";") 
152 
(Utils.fprintf_list ~sep:", " Printers.pp_var) ee.mmmemory 
153 
(Utils.fprintf_list ~sep:", " (fun fmt (o1, o2) > Format.fprintf fmt "(%s, %a)" o1 pp_static_call o2)) ee.mminstances 
154 
(Utils.fprintf_list ~sep:"@ " pp_instr) ee.mminit 
155 
pp_step ee.mmstep_logic 
156 
pp_step ee.mmstep_effects 
157  
158  
159 
let pp_spec fmt spec = 
160 
Format.fprintf fmt "@[<hov 2>(*@@ "; 
161 
Utils.fprintf_list ~sep:"@;@@ " (fun fmt r > Format.fprintf fmt "requires %a;" pp_eexpr r) fmt spec.m_requires; 
162 
Utils.fprintf_list ~sep:"@;@@ " (fun fmt r > Format.fprintf fmt "ensures %a; " pp_eexpr r) fmt spec.m_ensures; 
163 
Utils.fprintf_list ~sep:"@;" (fun fmt (name, assumes, ensures) > 
164 
Format.fprintf fmt "behavior %s:@[@ %a@ %a@]" 
165 
name 
166 
(Utils.fprintf_list ~sep:"@ " (fun fmt r > Format.fprintf fmt "assumes %a;" pp_eexpr r)) assumes 
167 
(Utils.fprintf_list ~sep:"@ " (fun fmt r > Format.fprintf fmt "ensures %a;" pp_eexpr r)) ensures 
168 
) fmt spec.m_behaviors; 
169 
Format.fprintf fmt "@]*)"; 
170 
() 
171  
172  
173  
174  
175 
let pp_machine fmt m = 
176 
Format.fprintf fmt 
177 
"@[<v 2>machine %s@;mem : %a@;instances: %a@;init : %a@;step :@; @[<v 2>%a@]@;spec: %a@;@]@ " 
178 
m.mname.node_id 
179 
(Utils.fprintf_list ~sep:", " Printers.pp_var) m.mmemory 
180 
(Utils.fprintf_list ~sep:", " (fun fmt (o1, o2) > Format.fprintf fmt "(%s, %a)" o1 pp_static_call o2)) m.minstances 
181 
(Utils.fprintf_list ~sep:"@ " pp_instr) m.minit 
182 
pp_step m.mstep 
183 
(fun fmt s > match s with None > ()  Some s > pp_spec fmt s) m.mspec 
184  
185 
let is_output m id = 
186 
List.exists (fun o > o.var_id = id.var_id) m.mstep.step_outputs 
187  
188 
let conditional c t e = 
189 
MBranch(c, [ (tag_true, t); (tag_false, e) ]) 
190  
191 
let dummy_var_decl name typ = 
192 
{ 
193 
var_id = name; 
194 
var_dec_type = dummy_type_dec; 
195 
var_dec_clock = dummy_clock_dec; 
196 
var_dec_const = false; 
197 
var_type = typ; 
198 
var_clock = Clocks.new_ck (Clocks.Cvar Clocks.CSet_all) true; 
199 
var_loc = Location.dummy_loc 
200 
} 
201  
202 
let arrow_id = "_arrow" 
203  
204 
let arrow_typ = Types.new_ty Types.Tunivar 
205  
206 
let arrow_desc = 
207 
{ 
208 
node_id = arrow_id; 
209 
node_type = Type_predef.type_bin_poly_op; 
210 
node_clock = Clock_predef.ck_bin_univ; 
211 
node_inputs= [dummy_var_decl "_in1" arrow_typ; dummy_var_decl "_in2" arrow_typ]; 
212 
node_outputs= [dummy_var_decl "_out" arrow_typ]; 
213 
node_locals= []; 
214 
node_gencalls = []; 
215 
node_checks = []; 
216 
node_asserts = []; 
217 
node_eqs= []; 
218 
node_spec = None; 
219 
node_annot = []; } 
220  
221 
let arrow_top_decl = 
222 
{ 
223 
top_decl_desc = Node arrow_desc; 
224 
top_decl_loc = Location.dummy_loc 
225 
} 
226  
227 
let arrow_machine = 
228 
let state = "_first" in 
229 
let var_state = dummy_var_decl state (Types.new_ty Types.Tbool) in 
230 
let var_input1 = List.nth arrow_desc.node_inputs 0 in 
231 
let var_input2 = List.nth arrow_desc.node_inputs 1 in 
232 
let var_output = List.nth arrow_desc.node_outputs 0 in 
233 
{ 
234 
mname = arrow_desc; 
235 
mmemory = [var_state]; 
236 
mcalls = []; 
237 
minstances = []; 
238 
minit = [MStateAssign(var_state, Cst (const_of_bool true))]; 
239 
mstatic = []; 
240 
mstep = { 
241 
step_inputs = arrow_desc.node_inputs; 
242 
step_outputs = arrow_desc.node_outputs; 
243 
step_locals = []; 
244 
step_checks = []; 
245 
step_instrs = [conditional (StateVar var_state) 
246 
[MStateAssign(var_state, Cst (const_of_bool false)); 
247 
MLocalAssign(var_output, LocalVar var_input1)] 
248 
[MLocalAssign(var_output, LocalVar var_input2)] ] 
249 
}; 
250 
mspec = None; 
251 
mannot = []; 
252 
} 
253  
254 
let is_stateless_node node = 
255 
(node_name node <> arrow_id) && 
256 
match node.top_decl_desc with 
257 
 Node id > false (* TODO: add a check after the machines are produced. Start from the main node and do a DFS to compute the stateless/statefull property of nodes. Stateless nodes should not be reset *) 
258 
 ImportedNode id > id.nodei_stateless 
259 
 ImportedFun _ > true 
260 
 _ > assert false 
261  
262 
let new_instance = 
263 
let cpt = ref (1) in 
264 
fun caller callee tag > 
265 
begin 
266 
let o = 
267 
if is_stateless_node callee then 
268 
node_name callee 
269 
else 
270 
Printf.sprintf "ni_%d" (incr cpt; !cpt) in 
271 
let o = 
272 
if !Options.ansi && is_generic_node callee 
273 
then Printf.sprintf "%s_inst_%d" o (Utils.position (fun e > e.expr_tag = tag) caller.node_gencalls) 
274 
else o in 
275 
o 
276 
end 
277  
278 
let const_of_carrier cr = 
279 
match (carrier_repr cr).carrier_desc with 
280 
 Carry_const id > id 
281 
 Carry_name > assert false 
282 
 Carry_var > assert false 
283 
 Carry_link _ > assert false (* TODO check this Xavier *) 
284  
285 
(* translate_<foo> : node > context > <foo> > machine code/expression *) 
286 
(* the context contains m : state aka memory variables *) 
287 
(* si : initialization instructions *) 
288 
(* j : node aka machine instances *) 
289 
(* d : local variables *) 
290 
(* s : step instructions *) 
291 
let translate_ident vars (m, si, j, d, s) id = 
292 
try (* id is a node var *) 
293 
(* Format.eprintf "translate ident: %s@.@?" id; *) 
294 
let var_id = try List.find (fun v > v.var_id= id) vars with Not_found > assert false in 
295 
if ISet.exists (fun v > v.var_id = id) m 
296 
then StateVar var_id 
297 
else LocalVar var_id 
298 
with Not_found > (* id is a constant *) 
299 
LocalVar (Corelang.var_decl_of_const (Hashtbl.find Corelang.consts_table id)) 
300  
301 
let rec control_on_clock vars ((m, si, j, d, s) as args) ck inst = 
302 
match ck.cdesc with 
303 
 Con (ck1, cr, l) > 
304 
let id = const_of_carrier cr in 
305 
control_on_clock vars args ck1 (MBranch (translate_ident vars args id, 
306 
[l, [inst]] )) 
307 
 _ > inst 
308  
309 
let rec join_branches hl1 hl2 = 
310 
match hl1, hl2 with 
311 
 [] , _ > hl2 
312 
 _ , [] > hl1 
313 
 (t1, h1)::q1, (t2, h2)::q2 > 
314 
if t1 < t2 then (t1, h1) :: join_branches q1 hl2 else 
315 
if t1 > t2 then (t2, h2) :: join_branches hl1 q2 
316 
else (t1, List.fold_right join_guards h1 h2) :: join_branches q1 q2 
317  
318 
and join_guards inst1 insts2 = 
319 
match inst1, insts2 with 
320 
 _ , [] > 
321 
[inst1] 
322 
 MBranch (x1, hl1), MBranch (x2, hl2) :: q when x1 = x2 > 
323 
MBranch (x1, join_branches (sort_handlers hl1) (sort_handlers hl2)) 
324 
:: q 
325 
 _ > inst1 :: insts2 
326  
327 
let join_guards_list insts = 
328 
List.fold_right join_guards insts [] 
329  
330 
let find_eq x eqs = 
331 
let rec aux accu eqs = 
332 
match eqs with 
333 
 [] > 
334 
begin 
335 
Format.eprintf "Looking for variable %a in the following equations@.%a@.@?" 
336 
Format.pp_print_string x 
337 
Printers.pp_node_eqs eqs; 
338 
assert false 
339 
end 
340 
 hd::tl > 
341 
if List.mem x hd.eq_lhs then hd, accu@tl else aux (hd::accu) tl 
342 
in 
343 
aux [] eqs 
344  
345 
let rec translate_expr vars ((m, si, j, d, s) as args) expr = 
346 
match expr.expr_desc with 
347 
 Expr_const v > Cst v 
348 
 Expr_ident x > translate_ident vars args x 
349 
 Expr_array el > Array (List.map (translate_expr vars args) el) 
350 
 Expr_access (t, i) > Access (translate_expr vars args t, translate_expr vars args (expr_of_dimension i)) 
351 
 Expr_power (e, n) > Power (translate_expr vars args e, translate_expr vars args (expr_of_dimension n)) 
352 
 Expr_tuple _ 
353 
 Expr_arrow _ 
354 
 Expr_fby _ 
355 
 Expr_pre _ > (Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError) 
356 
 Expr_when (e1, _, _) > translate_expr vars args e1 
357 
 Expr_merge (x, _) > raise NormalizationError 
358 
 Expr_appl (id, e, _) when Basic_library.is_internal_fun id > 
359 
let nd = node_from_name id in 
360 
(match e.expr_desc with 
361 
 Expr_tuple el > Fun (node_name nd, List.map (translate_expr vars args) el) 
362 
 _ > Fun (node_name nd, [translate_expr vars args e])) 
363 
 Expr_ite (g,t,e) > ( 
364 
(* special treatment depending on the active backend. For horn backend or 
365 
acsl spec, ite are preserved in expression. While they are removed for C 
366 
or Java backends. *) 
367 
Fun ("ite", [translate_expr vars args g; translate_expr vars args t; translate_expr vars args e]) 
368 
) 
369 
 _ > raise NormalizationError 
370  
371 
let translate_guard node args expr = 
372 
match expr.expr_desc with 
373 
 Expr_ident x > translate_ident node args x 
374 
 _ > assert false 
375  
376 
let rec translate_act node ((m, si, j, d, s) as args) (y, expr) = 
377 
match expr.expr_desc with 
378 
 Expr_ite (c, t, e) > let g = translate_guard node args c in 
379 
conditional g [translate_act node args (y, t)] 
380 
[translate_act node args (y, e)] 
381 
 Expr_merge (x, hl) > MBranch (translate_ident node args x, List.map (fun (t, h) > t, [translate_act node args (y, h)]) hl) 
382 
 _ > MLocalAssign (y, translate_expr node args expr) 
383  
384 
let reset_instance vars args i r c = 
385 
match r with 
386 
 None > [] 
387 
 Some (x, l) > [control_on_clock vars args c (MBranch (translate_ident vars args x, [l, [MReset i]]))] 
388  
389 
let translate_eq node keep_ite (local_vars: var_decl list) ((m, si, j, d, s) as args) eq = 
390 
(*Format.eprintf "translate_eq %a@." Printers.pp_node_eq eq;*) 
391 
let vars = local_vars@(node_vars node) in 
392 
let get_var x = 
393 
let test v = v.var_id = x in 
394 
if List.exists test vars then List.find test vars else assert false in 
395 
match eq.eq_lhs, eq.eq_rhs.expr_desc with 
396 
 [x], Expr_arrow (e1, e2) > 
397 
let var_x = get_var x in 
398 
let o = new_instance node arrow_top_decl eq.eq_rhs.expr_tag in 
399 
let c1 = translate_expr vars args e1 in 
400 
let c2 = translate_expr vars args e2 in 
401 
(m, 
402 
MReset o :: si, 
403 
Utils.IMap.add o (arrow_top_decl, []) j, 
404 
d, 
405 
(control_on_clock vars args eq.eq_rhs.expr_clock (MStep ([var_x], o, [c1;c2]))) :: s) 
406 
 [x], Expr_pre e1 when ISet.mem (get_var x) d > 
407 
let var_x = get_var x in 
408 
(ISet.add var_x m, 
409 
si, 
410 
j, 
411 
d, 
412 
control_on_clock vars args eq.eq_rhs.expr_clock (MStateAssign (var_x, translate_expr vars args e1)) :: s) 
413 
 [x], Expr_fby (e1, e2) when ISet.mem (get_var x) d > 
414 
let var_x = get_var x in 
415 
(ISet.add var_x m, 
416 
MStateAssign (var_x, translate_expr vars args e1) :: si, 
417 
j, 
418 
d, 
419 
control_on_clock vars args eq.eq_rhs.expr_clock (MStateAssign (var_x, translate_expr vars args e2)) :: s) 
420 
 p, Expr_appl (f, arg, r) > 
421 
let var_p = List.map (fun v > get_var v) p in 
422 
let el = 
423 
match arg.expr_desc with 
424 
 Expr_tuple el > el 
425 
 _ > [arg] in 
426 
let vl = List.map (translate_expr vars args) el in 
427 
let node_f = node_from_name f in 
428 
let call_f = 
429 
node_f, 
430 
NodeDep.filter_static_inputs (node_inputs node_f) el in 
431 
let o = new_instance node node_f eq.eq_rhs.expr_tag in 
432 
(m, 
433 
(if is_stateless_node node_f then si else MReset o :: si), 
434 
(if Basic_library.is_internal_fun f then j else Utils.IMap.add o call_f j), 
435 
d, 
436 
reset_instance vars args o r eq.eq_rhs.expr_clock @ 
437 
(control_on_clock vars args eq.eq_rhs.expr_clock (MStep (var_p, o, vl))) :: s) 
438  
439 
(* special treatment depending on the active backend. For horn backend, x = ite (g,t,e) 
440 
are preserved. While they are replaced as if g then x = t else x = e in C or Java 
441 
backends. *) 
442 
 [x], Expr_ite (c, t, e) when keep_ite > 
443 
let var_x = get_var x in 
444 
(m, 
445 
si, 
446 
j, 
447 
d, 
448 
(control_on_clock vars args eq.eq_rhs.expr_clock 
449 
(MLocalAssign (var_x, translate_expr vars args eq.eq_rhs))::s) 
450 
) 
451 

452 
 [x], _ > ( 
453 
let var_x = get_var x in 
454 
(m, si, j, d, 
455 
control_on_clock vars args eq.eq_rhs.expr_clock (translate_act vars args (var_x, eq.eq_rhs)) :: s) 
456 
) 
457 
 _ > 
458 
begin 
459 
Format.eprintf "unsupported equation: %a@?" Printers.pp_node_eq eq; 
460 
assert false 
461 
end 
462  
463 
let translate_eqs node keep_ite local_vars args eqs = 
464 
List.fold_right (fun eq args > translate_eq node keep_ite local_vars args eq) eqs args;; 
465  
466  
467 
(* The eexpr shoud have been normalized, ie. its eexpr_normalized field updated 
468 
We add a new boolean output var and bound it to the main expression 
469 
characterizing the eexpr. 
470 

471 
*) 
472 
let translate_eexpr nd eexpr = 
473 
(* Format.eprintf "Translating eexpr: %a" Printers.pp_eexpr eexpr; *) 
474 
let output_var, eqs, locals = match eexpr.eexpr_normalized with None > assert false  Some x > x in 
475 
(* both inputs and outputs are considered here as inputs for the specification *) 
476 
let inputs = nd.node_inputs @ nd.node_outputs in 
477 
let inputs_quantifiers = inputs @ (List.flatten (List.map snd eexpr.eexpr_quantifiers)) in 
478 

479 
let eexpr_local_vars = output_var :: locals @ (List.flatten (List.map snd eexpr.eexpr_quantifiers)) in 
480 
let visible_vars = eexpr_local_vars @ inputs in 
481 

482 
let sort_eqs inputs eqs = 
483 
let eqs_logic, new_locals_logic, sch_logic = Scheduling.schedule_eqs inputs visible_vars eqs in 
484 
(* Format.eprintf "sch: [%a]@;new locals: [%a]@;locals:[%a]@.eexpr local vars: [%a]@.@?" *) 
485 
(* (Utils.fprintf_list ~sep:", " Format.pp_print_string) sch_logic *) 
486 
(* (Utils.fprintf_list ~sep:", " Printers.pp_var) new_locals_logic *) 
487 
(* (Utils.fprintf_list ~sep:", " Printers.pp_var) locals *) 
488 
(* (Utils.fprintf_list ~sep:", " Printers.pp_var) eexpr_local_vars; *) 
489 
let locals = eexpr_local_vars @ new_locals_logic @ (List.flatten (List.map snd eexpr.eexpr_quantifiers)) in 
490 
let sorted_eqs_rev_logic, remainder_logic = 
491 
List.fold_left 
492 
(fun (accu, eqs_remainder) v > 
493 
if List.exists (fun eq > List.mem v eq.eq_lhs) accu 
494 
then (* The variable was already handled by a previous selected eq. 
495 
Typically it is part of a tuple *) 
496 
((* Format.eprintf "Case 1 for variable %s@." v; *) 
497 
(accu, eqs_remainder) 
498 
) 
499 
else if List.exists (fun vdecl > vdecl.var_id = v) locals  output_var.var_id = v 
500 
then ((* Select the eq associated to v. *) 
501 
(* Format.eprintf "Case 2 for variable %s@." v; *) 
502 
let eq_v, remainder = find_eq v eqs_remainder in 
503 
eq_v::accu, remainder 
504 
) 
505 
else ((* else it is a constant value, checked during typing phase *) 
506 
(* Format.eprintf "Case 3 for variable %s@." v; *) 
507 
accu, eqs_remainder 
508 
) 
509 
) 
510 
([], eqs_logic) 
511 
sch_logic 
512 
in 
513 
if List.length remainder_logic > 0 then ( 
514 
Format.eprintf "Spec equations not used are@.%a@.Full equation set is:@.%a@.@?" 
515 
Printers.pp_node_eqs remainder_logic 
516 
Printers.pp_node_eqs eqs_logic; 
517 
assert false ); 
518 
List.rev sorted_eqs_rev_logic, locals 
519 
in 
520  
521  
522 

523 
(* Generating logic definition instructions *) 
524 
let sorted_eqs, locals = sort_eqs inputs_quantifiers eqs in 
525  
526 
let init_args = 
527 
ISet.empty, 
528 
[], 
529 
Utils.IMap.empty, 
530 
List.fold_right (fun l > ISet.add l) locals ISet.empty, 
531 
[] 
532 
in 
533  
534 
let m, init, j, locals, s_logic = 
535 
translate_eqs nd true (* keep_ite *) eexpr_local_vars init_args (sorted_eqs) 
536 
in 
537  
538 
(* We remove side effects *) 
539 
let s_logic = List.filter (fun i > match i with MStateAssign _ > false  _ > true) s_logic in 
540 
(* and put the output var as the last instr *) 
541 
let s_logic = 
542 
let output_assign, others = 
543 
List.partition 
544 
(fun i > match i with  MStep([v], _, _)  MLocalAssign(v,_) > v.var_id = output_var.var_id  _ > false) 
545 
s_logic 
546 
in 
547 
(* Format.eprintf "output instr: @.%a@.others:@.%a@." *) 
548 
(* (Utils.fprintf_list ~sep:"@." pp_instr) output_assign *) 
549 
(* (Utils.fprintf_list ~sep:"@." pp_instr) others; *) 
550 
others @ output_assign 
551 
in 
552 
let _,_,_,_, s_side_effects = 
553 
translate_eqs nd false (* explose ite *) eexpr_local_vars init_args (sorted_eqs) 
554 
in 
555 
let rec filter_side_effects instrs = 
556 
List.fold_right ( 
557 
fun i accu > 
558 
match i with 
559 
 MStep([v], _, _) 
560 
 MLocalAssign(v,_) > 
561 
if v.var_id <> output_var.var_id then 
562 
i::accu 
563 
else 
564 
accu 
565 
 MBranch (g, cases) > 
566 
let filtered_cases = 
567 
List.map (fun (l, l_instrs) > l, filter_side_effects l_instrs) cases in 
568 
MBranch(g, filtered_cases) :: accu 
569 
 _ > i::accu 
570 

571 
) instrs [] 
572 
in 
573  
574  
575 
let s_side_effects = filter_side_effects s_side_effects in 
576 

577 
{ 
578 
muid = eexpr.eexpr_tag; 
579 
mquantifiers = eexpr.eexpr_quantifiers; 
580 
mmmemory = ISet.elements m; 
581 
mmcalls = []; (* no calls *) 
582 
mminstances = []; (* no calls *) 
583 
mminit = init; 
584 
mmstep_logic = { 
585 
step_inputs = inputs; 
586 
step_outputs = [output_var]; 
587 
step_locals = ISet.elements (ISet.remove output_var (ISet.diff locals m)); 
588 
step_checks = [] (* Not handled yet *); 
589 
step_instrs = ( 
590 
(* special treatment depending on the active backend. For horn backend, 
591 
common branches are not merged while they are in C or Java 
592 
backends. *) 
593 
match !Options.output with 
594 
 "C"  "horn" > s_logic 
595 
 "java"  _ > join_guards_list s_logic 
596 
) 
597 
}; 
598 
mmstep_effects = { 
599 
step_inputs = inputs; 
600 
step_outputs = []; 
601 
step_locals = ISet.elements (ISet.remove output_var (ISet.diff locals m)); 
602 
step_checks = [] (* Not handled yet *); 
603 
step_instrs = ( 
604 
(* special treatment depending on the active backend. For horn backend, 
605 
common branches are not merged while they are in C or Java 
606 
backends. *) 
607 
match !Options.output with 
608 
 "C"  "horn" > s_side_effects 
609 
 "java"  _ > join_guards_list s_side_effects 
610 
) 
611 
} 
612 
} 
613  
614  
615 
let translate_spec nd spec = 
616 
(* Each eexpr of the spec is expressed as a minimachine: 
617 
instrs (to update memory and set local vars) 
618 
+ expr (to compute the output 
619 
+ memory defs 
620 
+ instances (for callee nodes) 
621 
*) 
622 
let transl = List.map (translate_eexpr nd) in 
623 
{ 
624 
m_requires = transl spec.requires; 
625 
m_ensures = transl spec.ensures; 
626 
m_behaviors = 
627 
List.map 
628 
(fun (beh_id, req, ens, _) > beh_id, transl req, transl ens) 
629 
spec.behaviors 
630 
} 
631 

632 
let translate_decl top = 
633 
let nd = match top.top_decl_desc with Node nd > nd  _ > assert false in 
634 
(*Log.report ~level:1 (fun fmt > Printers.pp_node fmt nd);*) 
635 
let nd, sch = Scheduling.schedule_node nd in 
636 
(* Format.eprintf "node sch: [%a]@.@?" *) 
637 
(* (Utils.fprintf_list ~sep:", " Format.pp_print_string) sch; *) 
638  
639 
(* let split_eqs = Splitting.tuple_split_eq_list nd.node_eqs in *) 
640 
let sorted_eqs_rev, remainder = 
641 
List.fold_left 
642 
(fun (accu, node_eqs_remainder) v > 
643 
if List.exists (fun eq > List.mem v eq.eq_lhs) accu 
644 
then (* The variable was already handled by a previous selected eq. 
645 
Typically it is part of a tuple *) 
646 
(accu, node_eqs_remainder) 
647 
else 
648 
if List.exists (fun vdecl > vdecl.var_id = v) nd.node_locals 
649 
 List.exists (fun vdecl > vdecl.var_id = v) nd.node_outputs 
650 
then (* Select the eq associated to v. *) 
651 
let eq_v, remainder = find_eq v node_eqs_remainder in 
652 
eq_v::accu, remainder 
653 
else (* else it is a constant value, checked during typing phase *) 
654 
accu, node_eqs_remainder 
655 
) 
656 
([], nd.node_eqs) 
657 
sch 
658 
in 
659 
if List.length remainder > 0 then ( 
660 
Format.eprintf "Equations not used are@.%a@.Full equation set is:@.%a@.@?" 
661 
Printers.pp_node_eqs remainder 
662 
Printers.pp_node_eqs nd.node_eqs; 
663 
assert false ) 
664 
; 
665  
666 
let init_args = ISet.empty, [], Utils.IMap.empty, List.fold_right (fun l > ISet.add l) nd.node_locals ISet.empty, [] in 
667 
let keep_ite = (match !Options.output with  "horn"  "C" > true  "java"  _ > false) in 
668 
let m, init, j, locals, s = translate_eqs nd keep_ite [] init_args (List.rev sorted_eqs_rev) in 
669 
let mmap = Utils.IMap.fold (fun i n res > (i, n)::res) j [] in 
670 
{ 
671 
mname = nd; 
672 
mmemory = ISet.elements m; 
673 
mcalls = mmap; 
674 
minstances = List.filter (fun (_, (n,_)) > not (is_stateless_node n)) mmap; 
675 
minit = init; 
676 
mstatic = List.filter (fun v > v.var_dec_const) nd.node_inputs; 
677 
mstep = { 
678 
step_inputs = nd.node_inputs; 
679 
step_outputs = nd.node_outputs; 
680 
step_locals = ISet.elements (ISet.diff locals m); 
681 
step_checks = List.map (fun d > d.Dimension.dim_loc, translate_expr (node_vars nd) init_args (expr_of_dimension d)) nd.node_checks; 
682 
step_instrs = ( 
683 
(* special treatment depending on the active backend. For horn backend, 
684 
common branches are not merged while they are in C or Java 
685 
backends. *) 
686 
match !Options.output with 
687 
 "C"  "horn" > s 
688 
 "java"  _ > join_guards_list s 
689 
); 
690 
}; 
691 
mspec = Utils.option_map (translate_spec nd) nd.node_spec; 
692 
mannot = List.flatten ( 
693 
List.map (fun ann > List.map (fun (kwd, eexpr) > kwd, (translate_eexpr nd eexpr)) ann.annots) nd.node_annot); 
694 
} 
695 

696  
697 
let translate_prog decls = 
698 
let nodes = get_nodes decls in 
699 
arrow_machine :: List.map translate_decl nodes 
700  
701 
let get_machine_opt name machines = 
702 
List.fold_left 
703 
(fun res m > 
704 
match res with 
705 
 Some _ > res 
706 
 None > if m.mname.node_id = name then Some m else None) 
707 
None machines 
708 

709  
710 
let get_machine machines node = 
711 
let node = 
712 
(match node.top_decl_desc with 
713 
 Node nd > nd  _ > assert false) in 
714 
(match get_machine_opt node.node_id machines with 
715 
 None > assert false  Some m'> m') 
716  
717 
let rec get_mems m machines = 
718 
(* TODO: what to do with mcalls ? *) 
719 
(List.map (fun v > [], v) m.mmemory)@ 
720 
(List.flatten 
721 
(List.map 
722 
(fun (id, (node, _)) > 
723 
let m' = get_machine machines node in 
724 
let mems_m' = get_mems m' machines in 
725 
List.map (fun (prefix, var) > (id::prefix), var) mems_m') 
726 
m.minstances)) 
727  
728 
let rec get_instances m machines = 
729 
(* TODO: what to do with mcalls ? *) 
730 
let res = List.flatten 
731 
(List.map 
732 
(fun (id, (node, _)) > 
733 
let m' = get_machine machines node in 
734 
let instances_m' = get_instances m' machines in 
735 
match instances_m' with 
736 
 [] > [[id]] 
737 
 _ > [id]::(List.map (fun prefix > id::prefix) instances_m')) 
738 
m.minstances) 
739 
in 
740 
Format.eprintf "Instance of machine %s: %a@.@?" 
741 
m.mname.node_id 
742 
(Utils.fprintf_list ~sep:", " 
743 
(fun fmt l > Utils.fprintf_list ~sep:"" (fun fmt s > Format.fprintf fmt ">%s" s) fmt l)) res; 
744 
res 
745  
746 
let rec is_stateless_machine machines m = 
747 
(* no memories *) 
748 
m.mmemory = [] 
749 
(* all node instances are stateless *) 
750 
&& is_stateless_instances_list machines m.minstances 
751 
(* no spec memories *) 
752 
&& (match m.mspec with None > true  Some s > List.for_all (is_stateless_spec_machine machines) (s.m_requires @ s.m_ensures @ (List.fold_left (fun accu (_, assumes, requires) > accu @ assumes @ requires) [] s.m_behaviors))) 
753 
and is_stateless_spec_machine machines mm = 
754 
mm.mmmemory = [] 
755 
&& is_stateless_instances_list machines mm.mminstances 
756 
and is_stateless_instances_list machines = 
757 
List.for_all (fun (_, (node, _)) > 
758 
let node = 
759 
(match node.top_decl_desc with 
760 
 Node nd > nd  _ > assert false) in 
761 
let m' = 
762 
(match get_machine_opt node.node_id machines with 
763 
 None > assert false  Some m'> m') in 
764 
is_stateless_machine machines m' 
765 
) 
766  
767 
(* Local Variables: *) 
768 
(* compilecommand:"make C .." *) 
769 
(* End: *) 