Revision 3b2bd83d
Added by Teme Kahsai about 8 years ago
src/machine_code.ml | ||
---|---|---|
21 | 21 |
|
22 | 22 |
module ISet = Set.Make(OrdVarDecl) |
23 | 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 | 24 |
let rec pp_val fmt v = |
41 |
match v with |
|
42 |
| Cst c -> Printers.pp_const fmt c |
|
25 |
match v.value_desc with
|
|
26 |
| Cst c -> Printers.pp_const fmt c
|
|
43 | 27 |
| LocalVar v -> Format.pp_print_string fmt v.var_id |
44 | 28 |
| StateVar v -> Format.pp_print_string fmt v.var_id |
45 | 29 |
| Array vl -> Format.fprintf fmt "[%a]" (Utils.fprintf_list ~sep:", " pp_val) vl |
... | ... | |
52 | 36 |
| MLocalAssign (i,v) -> Format.fprintf fmt "%s<-l- %a" i.var_id pp_val v |
53 | 37 |
| MStateAssign (i,v) -> Format.fprintf fmt "%s<-s- %a" i.var_id pp_val v |
54 | 38 |
| MReset i -> Format.fprintf fmt "reset %s" i |
39 |
| MNoReset i -> Format.fprintf fmt "noreset %s" i |
|
55 | 40 |
| MStep (il, i, vl) -> |
56 | 41 |
Format.fprintf fmt "%a = %s (%a)" |
57 | 42 |
(Utils.fprintf_list ~sep:", " (fun fmt v -> Format.pp_print_string fmt v.var_id)) il |
... | ... | |
61 | 46 |
Format.fprintf fmt "@[<v 2>case(%a) {@,%a@,}@]" |
62 | 47 |
pp_val g |
63 | 48 |
(Utils.fprintf_list ~sep:"@," pp_branch) hl |
49 |
| MComment s -> Format.pp_print_string fmt s |
|
64 | 50 |
|
65 | 51 |
and pp_branch fmt (t, h) = |
66 | 52 |
Format.fprintf fmt "@[<v 2>%s:@,%a@]" t (Utils.fprintf_list ~sep:"@," pp_instr) h |
... | ... | |
119 | 105 |
(fun fmt -> match m.mspec with | None -> () | Some spec -> Printers.pp_spec fmt spec) |
120 | 106 |
(Utils.fprintf_list ~sep:"@ " Printers.pp_expr_annot) m.mannot |
121 | 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 |
|
|
122 | 114 |
(* Returns the declared stateless status and the computed one. *) |
123 | 115 |
let get_stateless_status m = |
124 | 116 |
(m.mname.node_dec_stateless, Utils.desome m.mname.node_stateless) |
... | ... | |
144 | 136 |
var_dec_const = false; |
145 | 137 |
var_dec_value = None; |
146 | 138 |
var_type = typ; |
147 |
var_clock = Clocks.new_ck (Clocks.Cvar Clocks.CSet_all) true;
|
|
139 |
var_clock = Clocks.new_ck Clocks.Cvar true;
|
|
148 | 140 |
var_loc = Location.dummy_loc |
149 | 141 |
} |
150 | 142 |
|
... | ... | |
177 | 169 |
top_decl_loc = Location.dummy_loc |
178 | 170 |
} |
179 | 171 |
|
172 |
let mk_val v t = { value_desc = v; |
|
173 |
value_type = t; |
|
174 |
value_annot = None } |
|
175 |
|
|
180 | 176 |
let arrow_machine = |
181 | 177 |
let state = "_first" in |
182 | 178 |
let var_state = dummy_var_decl state (Types.new_ty Types.Tbool) in |
183 | 179 |
let var_input1 = List.nth arrow_desc.node_inputs 0 in |
184 | 180 |
let var_input2 = List.nth arrow_desc.node_inputs 1 in |
185 | 181 |
let var_output = List.nth arrow_desc.node_outputs 0 in |
182 |
let cst b = mk_val (Cst (const_of_bool b)) Type_predef.type_bool in |
|
183 |
let t_arg = Types.new_univar () in (* TODO Xavier: c'est bien la bonne def ? *) |
|
186 | 184 |
{ |
187 | 185 |
mname = arrow_desc; |
188 | 186 |
mmemory = [var_state]; |
189 | 187 |
mcalls = []; |
190 | 188 |
minstances = []; |
191 |
minit = [MStateAssign(var_state, Cst (const_of_bool true))]; |
|
192 |
mconst = []; |
|
189 |
minit = [MStateAssign(var_state, cst true)]; |
|
193 | 190 |
mstatic = []; |
191 |
mconst = []; |
|
194 | 192 |
mstep = { |
195 | 193 |
step_inputs = arrow_desc.node_inputs; |
196 | 194 |
step_outputs = arrow_desc.node_outputs; |
197 | 195 |
step_locals = []; |
198 | 196 |
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)] ]; |
|
197 |
step_instrs = [conditional (mk_val (StateVar var_state) Type_predef.type_bool) |
|
198 |
[MStateAssign(var_state, cst false); |
|
199 |
MLocalAssign(var_output, mk_val (LocalVar var_input1) t_arg)] |
|
200 |
[MLocalAssign(var_output, mk_val (LocalVar var_input2) t_arg)] ]; |
|
201 |
step_asserts = []; |
|
202 |
}; |
|
203 |
mspec = None; |
|
204 |
mannot = []; |
|
205 |
} |
|
206 |
|
|
207 |
let empty_desc = |
|
208 |
{ |
|
209 |
node_id = arrow_id; |
|
210 |
node_type = Types.bottom; |
|
211 |
node_clock = Clocks.bottom; |
|
212 |
node_inputs= []; |
|
213 |
node_outputs= []; |
|
214 |
node_locals= []; |
|
215 |
node_gencalls = []; |
|
216 |
node_checks = []; |
|
217 |
node_asserts = []; |
|
218 |
node_stmts= []; |
|
219 |
node_dec_stateless = true; |
|
220 |
node_stateless = Some true; |
|
221 |
node_spec = None; |
|
222 |
node_annot = []; } |
|
223 |
|
|
224 |
let empty_machine = |
|
225 |
{ |
|
226 |
mname = empty_desc; |
|
227 |
mmemory = []; |
|
228 |
mcalls = []; |
|
229 |
minstances = []; |
|
230 |
minit = []; |
|
231 |
mstatic = []; |
|
232 |
mconst = []; |
|
233 |
mstep = { |
|
234 |
step_inputs = []; |
|
235 |
step_outputs = []; |
|
236 |
step_locals = []; |
|
237 |
step_checks = []; |
|
238 |
step_instrs = []; |
|
203 | 239 |
step_asserts = []; |
204 | 240 |
}; |
205 | 241 |
mspec = None; |
... | ... | |
233 | 269 |
try (* id is a node var *) |
234 | 270 |
let var_id = get_node_var id node in |
235 | 271 |
if ISet.exists (fun v -> v.var_id = id) m |
236 |
then StateVar var_id
|
|
237 |
else LocalVar var_id
|
|
272 |
then mk_val (StateVar var_id) var_id.var_type
|
|
273 |
else mk_val (LocalVar var_id) var_id.var_type
|
|
238 | 274 |
with Not_found -> |
239 | 275 |
try (* id is a constant *) |
240 |
LocalVar (Corelang.var_decl_of_const (const_of_top (Hashtbl.find Corelang.consts_table id))) |
|
276 |
let vdecl = (Corelang.var_decl_of_const (const_of_top (Hashtbl.find Corelang.consts_table id))) in |
|
277 |
mk_val (LocalVar vdecl) vdecl.var_type |
|
241 | 278 |
with Not_found -> |
242 | 279 |
(* id is a tag *) |
243 |
Cst (Const_tag id) |
|
280 |
(* DONE construire une liste des enum declarés et alors chercher dedans la liste |
|
281 |
qui contient id *) |
|
282 |
try |
|
283 |
let typ = (typedef_of_top (Hashtbl.find Corelang.tag_table id)).tydef_id in |
|
284 |
mk_val (Cst (Const_tag id)) (Type_predef.type_const typ) |
|
285 |
with Not_found -> (Format.eprintf "internal error: Machine_code.translate_ident %s" id; |
|
286 |
assert false) |
|
244 | 287 |
|
245 | 288 |
let rec control_on_clock node ((m, si, j, d, s) as args) ck inst = |
246 | 289 |
match (Clocks.repr ck).cdesc with |
... | ... | |
292 | 335 |
| "C" -> specialize_to_c expr |
293 | 336 |
| _ -> expr |
294 | 337 |
|
295 |
let rec translate_expr ?(ite=false) node ((m, si, j, d, s) as args) expr =
|
|
338 |
let rec translate_expr node ((m, si, j, d, s) as args) expr = |
|
296 | 339 |
let expr = specialize_op expr in |
297 |
match expr.expr_desc with
|
|
298 |
| Expr_const v -> Cst v
|
|
299 |
| Expr_ident x -> translate_ident node args x
|
|
300 |
| Expr_array el -> Array (List.map (translate_expr node args) el)
|
|
301 |
| Expr_access (t, i) -> Access (translate_expr node args t, translate_expr node args (expr_of_dimension i))
|
|
302 |
| Expr_power (e, n) -> Power (translate_expr node args e, translate_expr node args (expr_of_dimension n))
|
|
303 |
| Expr_tuple _
|
|
304 |
| Expr_arrow _
|
|
305 |
| Expr_fby _
|
|
306 |
| Expr_pre _ -> (Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError)
|
|
307 |
| Expr_when (e1, _, _) -> translate_expr node args e1
|
|
308 |
| Expr_merge (x, _) -> raise NormalizationError
|
|
309 |
| Expr_appl (id, e, _) when Basic_library.is_internal_fun id ->
|
|
310 |
let nd = node_from_name id in
|
|
311 |
Fun (node_name nd, List.map (translate_expr node args) (expr_list_of_expr e))
|
|
312 |
| Expr_ite (g,t,e) -> (
|
|
313 |
(* special treatment depending on the active backend. For horn backend, ite
|
|
314 |
are preserved in expression. While they are removed for C or Java
|
|
315 |
backends. *)
|
|
316 |
match !Options.output with
|
|
317 |
| "horn" ->
|
|
318 |
Fun ("ite", [translate_expr node args g; translate_expr node args t; translate_expr node args e])
|
|
319 |
| ("C" | "java") when ite ->
|
|
320 |
Fun ("ite", [translate_expr node args g; translate_expr node args t; translate_expr node args e])
|
|
321 |
| _ ->
|
|
322 |
(Format.eprintf "option:%s@." !Options.output; Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError)
|
|
323 |
)
|
|
324 |
| _ -> raise NormalizationError
|
|
340 |
let value_desc =
|
|
341 |
match expr.expr_desc with
|
|
342 |
| Expr_const v -> Cst v
|
|
343 |
| Expr_ident x -> (translate_ident node args x).value_desc
|
|
344 |
| Expr_array el -> Array (List.map (translate_expr node args) el)
|
|
345 |
| Expr_access (t, i) -> Access (translate_expr node args t, translate_expr node args (expr_of_dimension i))
|
|
346 |
| Expr_power (e, n) -> Power (translate_expr node args e, translate_expr node args (expr_of_dimension n))
|
|
347 |
| Expr_tuple _
|
|
348 |
| Expr_arrow _
|
|
349 |
| Expr_fby _
|
|
350 |
| Expr_pre _ -> (Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError)
|
|
351 |
| Expr_when (e1, _, _) -> (translate_expr node args e1).value_desc
|
|
352 |
| Expr_merge (x, _) -> raise NormalizationError
|
|
353 |
| Expr_appl (id, e, _) when Basic_library.is_expr_internal_fun expr ->
|
|
354 |
let nd = node_from_name id in
|
|
355 |
Fun (node_name nd, List.map (translate_expr node args) (expr_list_of_expr e))
|
|
356 |
(*| Expr_ite (g,t,e) -> (
|
|
357 |
(* special treatment depending on the active backend. For horn backend, ite
|
|
358 |
are preserved in expression. While they are removed for C or Java
|
|
359 |
backends. *)
|
|
360 |
match !Options.output with | "horn" ->
|
|
361 |
Fun ("ite", [translate_expr node args g; translate_expr node args t; translate_expr node args e])
|
|
362 |
| "C" | "java" | _ ->
|
|
363 |
(Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError)
|
|
364 |
)*)
|
|
365 |
| _ -> raise NormalizationError
|
|
366 |
in
|
|
367 |
mk_val value_desc expr.expr_type
|
|
325 | 368 |
|
326 | 369 |
let translate_guard node args expr = |
327 | 370 |
match expr.expr_desc with |
... | ... | |
331 | 374 |
let rec translate_act node ((m, si, j, d, s) as args) (y, expr) = |
332 | 375 |
match expr.expr_desc with |
333 | 376 |
| Expr_ite (c, t, e) -> let g = translate_guard node args c in |
334 |
conditional g [translate_act node args (y, t)] |
|
377 |
conditional g |
|
378 |
[translate_act node args (y, t)] |
|
335 | 379 |
[translate_act node args (y, e)] |
336 |
| Expr_merge (x, hl) -> MBranch (translate_ident node args x, List.map (fun (t, h) -> t, [translate_act node args (y, h)]) hl)
|
|
337 |
| _ ->
|
|
338 |
MLocalAssign (y, translate_expr node args expr)
|
|
380 |
| Expr_merge (x, hl) -> MBranch (translate_ident node args x, |
|
381 |
List.map (fun (t, h) -> t, [translate_act node args (y, h)]) hl)
|
|
382 |
| _ -> MLocalAssign (y, translate_expr node args expr)
|
|
339 | 383 |
|
340 | 384 |
let reset_instance node args i r c = |
341 | 385 |
match r with |
342 | 386 |
| None -> [] |
343 | 387 |
| Some r -> let g = translate_guard node args r in |
344 |
[control_on_clock node args c (conditional g [MReset i] [])] |
|
388 |
[control_on_clock node args c (conditional g [MReset i] [MNoReset i])]
|
|
345 | 389 |
|
346 | 390 |
let translate_eq node ((m, si, j, d, s) as args) eq = |
347 | 391 |
(* Format.eprintf "translate_eq %a with clock %a@." Printers.pp_node_eq eq Clocks.print_ck eq.eq_rhs.expr_clock; *) |
... | ... | |
371 | 415 |
d, |
372 | 416 |
control_on_clock node args eq.eq_rhs.expr_clock (MStateAssign (var_x, translate_expr node args e2)) :: s) |
373 | 417 |
|
374 |
| p , Expr_appl (f, arg, r) when not (Basic_library.is_internal_fun f) ->
|
|
418 |
| p , Expr_appl (f, arg, r) when not (Basic_library.is_expr_internal_fun eq.eq_rhs) ->
|
|
375 | 419 |
let var_p = List.map (fun v -> get_node_var v node) p in |
376 | 420 |
let el = expr_list_of_expr arg in |
377 | 421 |
let vl = List.map (translate_expr node args) el in |
... | ... | |
393 | 437 |
then [] |
394 | 438 |
else reset_instance node args o r call_ck) @ |
395 | 439 |
(control_on_clock node args call_ck (MStep (var_p, o, vl))) :: s) |
396 |
|
|
440 |
(* |
|
397 | 441 |
(* special treatment depending on the active backend. For horn backend, x = ite (g,t,e) |
398 | 442 |
are preserved. While they are replaced as if g then x = t else x = e in C or Java |
399 | 443 |
backends. *) |
... | ... | |
409 | 453 |
(MLocalAssign (var_x, translate_expr node args eq.eq_rhs))::s) |
410 | 454 |
) |
411 | 455 |
|
456 |
*) |
|
412 | 457 |
| [x], _ -> ( |
413 | 458 |
let var_x = get_node_var x node in |
414 | 459 |
(m, si, j, d, |
... | ... | |
421 | 466 |
) |
422 | 467 |
| _ -> |
423 | 468 |
begin |
424 |
Format.eprintf "unsupported equation: %a@?" Printers.pp_node_eq eq;
|
|
469 |
Format.eprintf "internal error: Machine_code.translate_eq %a@?" Printers.pp_node_eq eq;
|
|
425 | 470 |
assert false |
426 | 471 |
end |
427 | 472 |
|
... | ... | |
444 | 489 |
to the computed schedule [sch] |
445 | 490 |
*) |
446 | 491 |
let sort_equations_from_schedule nd sch = |
447 |
(*Format.eprintf "%s schedule: %a@."
|
|
448 |
nd.node_id
|
|
449 |
(Utils.fprintf_list ~sep:" ; " Scheduling.pp_eq_schedule) sch;*)
|
|
492 |
(* Format.eprintf "%s schedule: %a@." *)
|
|
493 |
(* nd.node_id *)
|
|
494 |
(* (Utils.fprintf_list ~sep:" ; " Scheduling.pp_eq_schedule) sch; *)
|
|
450 | 495 |
let split_eqs = Splitting.tuple_split_eq_list (get_node_eqs nd) in |
451 | 496 |
let eqs_rev, remainder = |
452 | 497 |
List.fold_left |
... | ... | |
515 | 560 |
(* special treatment depending on the active backend. For horn backend, |
516 | 561 |
common branches are not merged while they are in C or Java |
517 | 562 |
backends. *) |
518 |
match !Options.output with |
|
563 |
(*match !Options.output with
|
|
519 | 564 |
| "horn" -> s |
520 |
| "C" | "java" | _ -> join_guards_list s |
|
565 |
| "C" | "java" | _ ->*) join_guards_list s
|
|
521 | 566 |
); |
522 | 567 |
step_asserts = |
523 | 568 |
let exprl = List.map (fun assert_ -> assert_.assert_expr ) nd.node_asserts in |
... | ... | |
554 | 599 |
with Not_found -> assert false |
555 | 600 |
|
556 | 601 |
|
557 |
let value_of_ident m id = |
|
602 |
let value_of_ident loc m id =
|
|
558 | 603 |
(* is is a state var *) |
559 | 604 |
try |
560 |
StateVar (List.find (fun v -> v.var_id = id) m.mmemory) |
|
605 |
let v = List.find (fun v -> v.var_id = id) m.mmemory |
|
606 |
in mk_val (StateVar v) v.var_type |
|
561 | 607 |
with Not_found -> |
562 |
try (* id is a node var *) |
|
563 |
LocalVar (get_node_var id m.mname) |
|
608 |
try (* id is a node var *) |
|
609 |
let v = get_node_var id m.mname |
|
610 |
in mk_val (LocalVar v) v.var_type |
|
564 | 611 |
with Not_found -> |
565 | 612 |
try (* id is a constant *) |
566 |
LocalVar (Corelang.var_decl_of_const (const_of_top (Hashtbl.find Corelang.consts_table id))) |
|
613 |
let c = Corelang.var_decl_of_const (const_of_top (Hashtbl.find Corelang.consts_table id)) |
|
614 |
in mk_val (LocalVar c) c.var_type |
|
567 | 615 |
with Not_found -> |
568 | 616 |
(* id is a tag *) |
569 |
Cst (Const_tag id) |
|
617 |
let t = Const_tag id |
|
618 |
in mk_val (Cst t) (Typing.type_const loc t) |
|
619 |
|
|
620 |
(* type of internal fun used in dimension expression *) |
|
621 |
let type_of_value_appl f args = |
|
622 |
if List.mem f Basic_library.arith_funs |
|
623 |
then (List.hd args).value_type |
|
624 |
else Type_predef.type_bool |
|
570 | 625 |
|
571 | 626 |
let rec value_of_dimension m dim = |
572 | 627 |
match dim.Dimension.dim_desc with |
573 |
| Dimension.Dbool b -> Cst (Const_tag (if b then Corelang.tag_true else Corelang.tag_false)) |
|
574 |
| Dimension.Dint i -> Cst (Const_int i) |
|
575 |
| Dimension.Dident v -> value_of_ident m v |
|
576 |
| Dimension.Dappl (f, args) -> Fun (f, List.map (value_of_dimension m) args) |
|
577 |
| Dimension.Dite (i, t, e) -> Fun ("ite", List.map (value_of_dimension m) [i; t; e]) |
|
628 |
| Dimension.Dbool b -> |
|
629 |
mk_val (Cst (Const_tag (if b then Corelang.tag_true else Corelang.tag_false))) Type_predef.type_bool |
|
630 |
| Dimension.Dint i -> |
|
631 |
mk_val (Cst (Const_int i)) Type_predef.type_int |
|
632 |
| Dimension.Dident v -> value_of_ident dim.Dimension.dim_loc m v |
|
633 |
| Dimension.Dappl (f, args) -> |
|
634 |
let vargs = List.map (value_of_dimension m) args |
|
635 |
in mk_val (Fun (f, vargs)) (type_of_value_appl f vargs) |
|
636 |
| Dimension.Dite (i, t, e) -> |
|
637 |
(match List.map (value_of_dimension m) [i; t; e] with |
|
638 |
| [vi; vt; ve] -> mk_val (Fun ("ite", [vi; vt; ve])) vt.value_type |
|
639 |
| _ -> assert false) |
|
578 | 640 |
| Dimension.Dlink dim' -> value_of_dimension m dim' |
579 | 641 |
| _ -> assert false |
580 | 642 |
|
581 | 643 |
let rec dimension_of_value value = |
582 |
match value with |
|
644 |
match value.value_desc with
|
|
583 | 645 |
| Cst (Const_tag t) when t = Corelang.tag_true -> Dimension.mkdim_bool Location.dummy_loc true |
584 | 646 |
| Cst (Const_tag t) when t = Corelang.tag_false -> Dimension.mkdim_bool Location.dummy_loc false |
585 | 647 |
| Cst (Const_int i) -> Dimension.mkdim_int Location.dummy_loc i |
Also available in: Unified diff
updating to onera version 30f766a:2016-12-04