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