Revision 2863281f
Added by Pierre-Loïc Garoche almost 7 years ago
src/machine_code.ml | ||
---|---|---|
11 | 11 |
|
12 | 12 |
open Lustre_types |
13 | 13 |
open Machine_code_types |
14 |
open Machine_code_common |
|
14 | 15 |
open Corelang |
15 | 16 |
open Clocks |
16 | 17 |
open Causality |
17 |
|
|
18 |
let print_statelocaltag = true |
|
19 | 18 |
|
20 | 19 |
exception NormalizationError |
21 | 20 |
|
22 | 21 |
|
23 |
let rec pp_val fmt v = |
|
24 |
match v.value_desc with |
|
25 |
| Cst c -> Printers.pp_const fmt c |
|
26 |
| LocalVar v -> |
|
27 |
if print_statelocaltag then |
|
28 |
Format.fprintf fmt "%s(L)" v.var_id |
|
29 |
else |
|
30 |
Format.pp_print_string fmt v.var_id |
|
31 |
|
|
32 |
| StateVar v -> |
|
33 |
if print_statelocaltag then |
|
34 |
Format.fprintf fmt "%s(S)" v.var_id |
|
35 |
else |
|
36 |
Format.pp_print_string fmt v.var_id |
|
37 |
| Array vl -> Format.fprintf fmt "[%a]" (Utils.fprintf_list ~sep:", " pp_val) vl |
|
38 |
| Access (t, i) -> Format.fprintf fmt "%a[%a]" pp_val t pp_val i |
|
39 |
| Power (v, n) -> Format.fprintf fmt "(%a^%a)" pp_val v pp_val n |
|
40 |
| Fun (n, vl) -> Format.fprintf fmt "%s (%a)" n (Utils.fprintf_list ~sep:", " pp_val) vl |
|
41 |
|
|
42 |
let rec pp_instr fmt i = |
|
43 |
let _ = |
|
44 |
match i.instr_desc with |
|
45 |
| MLocalAssign (i,v) -> Format.fprintf fmt "%s<-l- %a" i.var_id pp_val v |
|
46 |
| MStateAssign (i,v) -> Format.fprintf fmt "%s<-s- %a" i.var_id pp_val v |
|
47 |
| MReset i -> Format.fprintf fmt "reset %s" i |
|
48 |
| MNoReset i -> Format.fprintf fmt "noreset %s" i |
|
49 |
| MStep (il, i, vl) -> |
|
50 |
Format.fprintf fmt "%a = %s (%a)" |
|
51 |
(Utils.fprintf_list ~sep:", " (fun fmt v -> Format.pp_print_string fmt v.var_id)) il |
|
52 |
i |
|
53 |
(Utils.fprintf_list ~sep:", " pp_val) vl |
|
54 |
| MBranch (g,hl) -> |
|
55 |
Format.fprintf fmt "@[<v 2>case(%a) {@,%a@,}@]" |
|
56 |
pp_val g |
|
57 |
(Utils.fprintf_list ~sep:"@," pp_branch) hl |
|
58 |
| MComment s -> Format.pp_print_string fmt s |
|
59 |
|
|
60 |
in |
|
61 |
(* Annotation *) |
|
62 |
(* let _ = *) |
|
63 |
(* match i.lustre_expr with None -> () | Some e -> Format.fprintf fmt " -- original expr: %a" Printers.pp_expr e *) |
|
64 |
(* in *) |
|
65 |
let _ = |
|
66 |
match i.lustre_eq with None -> () | Some eq -> Format.fprintf fmt " -- original eq: %a" Printers.pp_node_eq eq |
|
67 |
in |
|
68 |
() |
|
69 |
|
|
70 |
and pp_branch fmt (t, h) = |
|
71 |
Format.fprintf fmt "@[<v 2>%s:@,%a@]" t (Utils.fprintf_list ~sep:"@," pp_instr) h |
|
72 |
|
|
73 |
and pp_instrs fmt il = |
|
74 |
Format.fprintf fmt "@[<v 2>%a@]" (Utils.fprintf_list ~sep:"@," pp_instr) il |
|
75 |
|
|
76 |
|
|
77 |
(* merge log: get_node_def was in c0f8 *) |
|
78 |
(* Returns the node/machine associated to id in m calls *) |
|
79 |
let get_node_def id m = |
|
80 |
try |
|
81 |
let (decl, _) = List.assoc id m.mcalls in |
|
82 |
Corelang.node_of_top decl |
|
83 |
with Not_found -> ( |
|
84 |
(* Format.eprintf "Unable to find node %s in list [%a]@.@?" *) |
|
85 |
(* id *) |
|
86 |
(* (Utils.fprintf_list ~sep:", " (fun fmt (n,_) -> Format.fprintf fmt "%s" n)) m.mcalls *) |
|
87 |
(* ; *) |
|
88 |
raise Not_found |
|
89 |
) |
|
90 |
|
|
91 |
(* merge log: machine_vars was in 44686 *) |
|
92 |
let machine_vars m = m.mstep.step_inputs @ m.mstep.step_locals @ m.mstep.step_outputs @ m.mmemory |
|
93 |
|
|
94 |
let pp_step fmt s = |
|
95 |
Format.fprintf fmt "@[<v>inputs : %a@ outputs: %a@ locals : %a@ checks : %a@ instrs : @[%a@]@ asserts : @[%a@]@]@ " |
|
96 |
(Utils.fprintf_list ~sep:", " Printers.pp_var) s.step_inputs |
|
97 |
(Utils.fprintf_list ~sep:", " Printers.pp_var) s.step_outputs |
|
98 |
(Utils.fprintf_list ~sep:", " Printers.pp_var) s.step_locals |
|
99 |
(Utils.fprintf_list ~sep:", " (fun fmt (_, c) -> pp_val fmt c)) s.step_checks |
|
100 |
(Utils.fprintf_list ~sep:"@ " pp_instr) s.step_instrs |
|
101 |
(Utils.fprintf_list ~sep:", " pp_val) s.step_asserts |
|
102 |
|
|
103 |
|
|
104 |
let pp_static_call fmt (node, args) = |
|
105 |
Format.fprintf fmt "%s<%a>" |
|
106 |
(node_name node) |
|
107 |
(Utils.fprintf_list ~sep:", " Dimension.pp_dimension) args |
|
108 |
|
|
109 |
let pp_machine fmt m = |
|
110 |
Format.fprintf fmt |
|
111 |
"@[<v 2>machine %s@ mem : %a@ instances: %a@ init : %a@ const : %a@ step :@ @[<v 2>%a@]@ @ spec : @[%t@]@ annot : @[%a@]@]@ " |
|
112 |
m.mname.node_id |
|
113 |
(Utils.fprintf_list ~sep:", " Printers.pp_var) m.mmemory |
|
114 |
(Utils.fprintf_list ~sep:", " (fun fmt (o1, o2) -> Format.fprintf fmt "(%s, %a)" o1 pp_static_call o2)) m.minstances |
|
115 |
(Utils.fprintf_list ~sep:"@ " pp_instr) m.minit |
|
116 |
(Utils.fprintf_list ~sep:"@ " pp_instr) m.mconst |
|
117 |
pp_step m.mstep |
|
118 |
(fun fmt -> match m.mspec with | None -> () | Some spec -> Printers.pp_spec fmt spec) |
|
119 |
(Utils.fprintf_list ~sep:"@ " Printers.pp_expr_annot) m.mannot |
|
120 |
|
|
121 |
let pp_machines fmt ml = |
|
122 |
Format.fprintf fmt "@[<v 0>%a@]" (Utils.fprintf_list ~sep:"@," pp_machine) ml |
|
123 |
|
|
124 |
|
|
125 |
let rec is_const_value v = |
|
126 |
match v.value_desc with |
|
127 |
| Cst _ -> true |
|
128 |
| Fun (id, args) -> Basic_library.is_value_internal_fun v && List.for_all is_const_value args |
|
129 |
| _ -> false |
|
130 |
|
|
131 |
(* Returns the declared stateless status and the computed one. *) |
|
132 |
let get_stateless_status m = |
|
133 |
(m.mname.node_dec_stateless, try Utils.desome m.mname.node_stateless with _ -> failwith ("stateless status of machine " ^ m.mname.node_id ^ " not computed")) |
|
134 |
|
|
135 |
let is_input m id = |
|
136 |
List.exists (fun o -> o.var_id = id.var_id) m.mstep.step_inputs |
|
137 |
|
|
138 |
let is_output m id = |
|
139 |
List.exists (fun o -> o.var_id = id.var_id) m.mstep.step_outputs |
|
140 |
|
|
141 |
let is_memory m id = |
|
142 |
List.exists (fun o -> o.var_id = id.var_id) m.mmemory |
|
143 |
|
|
144 |
let conditional ?lustre_eq c t e = |
|
145 |
mkinstr ?lustre_eq:lustre_eq (MBranch(c, [ (tag_true, t); (tag_false, e) ])) |
|
146 |
|
|
147 |
let dummy_var_decl name typ = |
|
148 |
{ |
|
149 |
var_id = name; |
|
150 |
var_orig = false; |
|
151 |
var_dec_type = dummy_type_dec; |
|
152 |
var_dec_clock = dummy_clock_dec; |
|
153 |
var_dec_const = false; |
|
154 |
var_dec_value = None; |
|
155 |
var_parent_nodeid = None; |
|
156 |
var_type = typ; |
|
157 |
var_clock = Clocks.new_ck Clocks.Cvar true; |
|
158 |
var_loc = Location.dummy_loc |
|
159 |
} |
|
160 |
|
|
161 |
let arrow_id = "_arrow" |
|
162 |
|
|
163 |
let arrow_typ = Types.new_ty Types.Tunivar |
|
164 |
|
|
165 |
let arrow_desc = |
|
166 |
{ |
|
167 |
node_id = arrow_id; |
|
168 |
node_type = Type_predef.type_bin_poly_op; |
|
169 |
node_clock = Clock_predef.ck_bin_univ; |
|
170 |
node_inputs= [dummy_var_decl "_in1" arrow_typ; dummy_var_decl "_in2" arrow_typ]; |
|
171 |
node_outputs= [dummy_var_decl "_out" arrow_typ]; |
|
172 |
node_locals= []; |
|
173 |
node_gencalls = []; |
|
174 |
node_checks = []; |
|
175 |
node_asserts = []; |
|
176 |
node_stmts= []; |
|
177 |
node_dec_stateless = false; |
|
178 |
node_stateless = Some false; |
|
179 |
node_spec = None; |
|
180 |
node_annot = []; } |
|
181 |
|
|
182 |
let arrow_top_decl = |
|
183 |
{ |
|
184 |
top_decl_desc = Node arrow_desc; |
|
185 |
top_decl_owner = (Options_management.core_dependency "arrow"); |
|
186 |
top_decl_itf = false; |
|
187 |
top_decl_loc = Location.dummy_loc |
|
188 |
} |
|
189 |
|
|
190 |
let mk_val v t = |
|
191 |
{ value_desc = v; |
|
192 |
value_type = t; |
|
193 |
value_annot = None } |
|
194 |
|
|
195 |
let arrow_machine = |
|
196 |
let state = "_first" in |
|
197 |
let var_state = dummy_var_decl state Type_predef.type_bool(* (Types.new_ty Types.Tbool) *) in |
|
198 |
let var_input1 = List.nth arrow_desc.node_inputs 0 in |
|
199 |
let var_input2 = List.nth arrow_desc.node_inputs 1 in |
|
200 |
let var_output = List.nth arrow_desc.node_outputs 0 in |
|
201 |
let cst b = mk_val (Cst (const_of_bool b)) Type_predef.type_bool in |
|
202 |
let t_arg = Types.new_univar () in (* TODO Xavier: c'est bien la bonne def ? *) |
|
203 |
{ |
|
204 |
mname = arrow_desc; |
|
205 |
mmemory = [var_state]; |
|
206 |
mcalls = []; |
|
207 |
minstances = []; |
|
208 |
minit = [mkinstr (MStateAssign(var_state, cst true))]; |
|
209 |
mstatic = []; |
|
210 |
mconst = []; |
|
211 |
mstep = { |
|
212 |
step_inputs = arrow_desc.node_inputs; |
|
213 |
step_outputs = arrow_desc.node_outputs; |
|
214 |
step_locals = []; |
|
215 |
step_checks = []; |
|
216 |
step_instrs = [conditional (mk_val (StateVar var_state) Type_predef.type_bool) |
|
217 |
(List.map mkinstr |
|
218 |
[MStateAssign(var_state, cst false); |
|
219 |
MLocalAssign(var_output, mk_val (LocalVar var_input1) t_arg)]) |
|
220 |
(List.map mkinstr |
|
221 |
[MLocalAssign(var_output, mk_val (LocalVar var_input2) t_arg)]) ]; |
|
222 |
step_asserts = []; |
|
223 |
}; |
|
224 |
mspec = None; |
|
225 |
mannot = []; |
|
226 |
} |
|
227 |
|
|
228 |
let empty_desc = |
|
229 |
{ |
|
230 |
node_id = arrow_id; |
|
231 |
node_type = Types.bottom; |
|
232 |
node_clock = Clocks.bottom; |
|
233 |
node_inputs= []; |
|
234 |
node_outputs= []; |
|
235 |
node_locals= []; |
|
236 |
node_gencalls = []; |
|
237 |
node_checks = []; |
|
238 |
node_asserts = []; |
|
239 |
node_stmts= []; |
|
240 |
node_dec_stateless = true; |
|
241 |
node_stateless = Some true; |
|
242 |
node_spec = None; |
|
243 |
node_annot = []; } |
|
244 |
|
|
245 |
let empty_machine = |
|
246 |
{ |
|
247 |
mname = empty_desc; |
|
248 |
mmemory = []; |
|
249 |
mcalls = []; |
|
250 |
minstances = []; |
|
251 |
minit = []; |
|
252 |
mstatic = []; |
|
253 |
mconst = []; |
|
254 |
mstep = { |
|
255 |
step_inputs = []; |
|
256 |
step_outputs = []; |
|
257 |
step_locals = []; |
|
258 |
step_checks = []; |
|
259 |
step_instrs = []; |
|
260 |
step_asserts = []; |
|
261 |
}; |
|
262 |
mspec = None; |
|
263 |
mannot = []; |
|
264 |
} |
|
265 |
|
|
266 |
let new_instance = |
|
267 |
let cpt = ref (-1) in |
|
268 |
fun caller callee tag -> |
|
269 |
begin |
|
270 |
let o = |
|
271 |
if Stateless.check_node callee then |
|
272 |
node_name callee |
|
273 |
else |
|
274 |
Printf.sprintf "ni_%d" (incr cpt; !cpt) in |
|
275 |
let o = |
|
276 |
if !Options.ansi && is_generic_node callee |
|
277 |
then Printf.sprintf "%s_inst_%d" o (Utils.position (fun e -> e.expr_tag = tag) caller.node_gencalls) |
|
278 |
else o in |
|
279 |
o |
|
280 |
end |
|
281 |
|
|
282 |
|
|
283 | 22 |
(* translate_<foo> : node -> context -> <foo> -> machine code/expression *) |
284 | 23 |
(* the context contains m : state aka memory variables *) |
285 | 24 |
(* si : initialization instructions *) |
... | ... | |
325 | 64 |
[l, [inst]] ))) |
326 | 65 |
| _ -> inst |
327 | 66 |
|
328 |
let rec join_branches hl1 hl2 = |
|
329 |
match hl1, hl2 with |
|
330 |
| [] , _ -> hl2 |
|
331 |
| _ , [] -> hl1 |
|
332 |
| (t1, h1)::q1, (t2, h2)::q2 -> |
|
333 |
if t1 < t2 then (t1, h1) :: join_branches q1 hl2 else |
|
334 |
if t1 > t2 then (t2, h2) :: join_branches hl1 q2 |
|
335 |
else (t1, List.fold_right join_guards h1 h2) :: join_branches q1 q2 |
|
336 |
|
|
337 |
and join_guards inst1 insts2 = |
|
338 |
match get_instr_desc inst1, List.map get_instr_desc insts2 with |
|
339 |
| _ , [] -> |
|
340 |
[inst1] |
|
341 |
| MBranch (x1, hl1), MBranch (x2, hl2) :: q when x1 = x2 -> |
|
342 |
mkinstr |
|
343 |
(* TODO on pourrait uniquement concatener les lustres de inst1 et hd(inst2) *) |
|
344 |
(MBranch (x1, join_branches (sort_handlers hl1) (sort_handlers hl2))) |
|
345 |
:: (List.tl insts2) |
|
346 |
| _ -> inst1 :: insts2 |
|
347 |
|
|
348 |
let join_guards_list insts = |
|
349 |
List.fold_right join_guards insts [] |
|
350 | 67 |
|
351 | 68 |
(* specialize predefined (polymorphic) operators |
352 | 69 |
wrt their instances, so that the C semantics |
... | ... | |
413 | 130 |
let eq = Corelang.mkeq Location.dummy_loc ([y.var_id], expr) in |
414 | 131 |
match expr.expr_desc with |
415 | 132 |
| Expr_ite (c, t, e) -> let g = translate_guard node args c in |
416 |
conditional ?lustre_eq:(Some eq) g |
|
133 |
mk_conditional ?lustre_eq:(Some eq) g
|
|
417 | 134 |
[translate_act node args (y, t)] |
418 | 135 |
[translate_act node args (y, e)] |
419 | 136 |
| Expr_merge (x, hl) -> mkinstr ?lustre_eq:(Some eq) (MBranch (translate_ident node args x, |
... | ... | |
424 | 141 |
match r with |
425 | 142 |
| None -> [] |
426 | 143 |
| Some r -> let g = translate_guard node args r in |
427 |
[control_on_clock node args c (conditional g [mkinstr (MReset i)] [mkinstr (MNoReset i)])] |
|
144 |
[control_on_clock node args c (mk_conditional g [mkinstr (MReset i)] [mkinstr (MNoReset i)])]
|
|
428 | 145 |
|
429 | 146 |
let translate_eq node ((m, si, j, d, s) as args) eq = |
430 | 147 |
(* Format.eprintf "translate_eq %a with clock %a@." Printers.pp_node_eq eq Clocks.print_ck eq.eq_rhs.expr_clock; *) |
431 | 148 |
match eq.eq_lhs, eq.eq_rhs.expr_desc with |
432 | 149 |
| [x], Expr_arrow (e1, e2) -> |
433 | 150 |
let var_x = get_node_var x node in |
434 |
let o = new_instance node arrow_top_decl eq.eq_rhs.expr_tag in |
|
151 |
let o = new_instance node Arrow.arrow_top_decl eq.eq_rhs.expr_tag in
|
|
435 | 152 |
let c1 = translate_expr node args e1 in |
436 | 153 |
let c2 = translate_expr node args e2 in |
437 | 154 |
(m, |
438 | 155 |
mkinstr (MReset o) :: si, |
439 |
Utils.IMap.add o (arrow_top_decl, []) j, |
|
156 |
Utils.IMap.add o (Arrow.arrow_top_decl, []) j,
|
|
440 | 157 |
d, |
441 | 158 |
(control_on_clock node args eq.eq_rhs.expr_clock (mkinstr ?lustre_eq:(Some eq) (MStep ([var_x], o, [c1;c2])))) :: s) |
442 | 159 |
| [x], Expr_pre e1 when VSet.mem (get_node_var x node) d -> |
... | ... | |
661 | 378 |
translate_decl node sch |
662 | 379 |
) nodes |
663 | 380 |
|
664 |
let get_machine_opt name machines = |
|
665 |
List.fold_left |
|
666 |
(fun res m -> |
|
667 |
match res with |
|
668 |
| Some _ -> res |
|
669 |
| None -> if m.mname.node_id = name then Some m else None) |
|
670 |
None machines |
|
671 |
|
|
672 |
let get_const_assign m id = |
|
673 |
try |
|
674 |
match get_instr_desc (List.find |
|
675 |
(fun instr -> match get_instr_desc instr with |
|
676 |
| MLocalAssign (v, _) -> v == id |
|
677 |
| _ -> false) |
|
678 |
m.mconst |
|
679 |
) with |
|
680 |
| MLocalAssign (_, e) -> e |
|
681 |
| _ -> assert false |
|
682 |
with Not_found -> assert false |
|
683 |
|
|
684 |
|
|
685 |
let value_of_ident loc m id = |
|
686 |
(* is is a state var *) |
|
687 |
try |
|
688 |
let v = List.find (fun v -> v.var_id = id) m.mmemory |
|
689 |
in mk_val (StateVar v) v.var_type |
|
690 |
with Not_found -> |
|
691 |
try (* id is a node var *) |
|
692 |
let v = get_node_var id m.mname |
|
693 |
in mk_val (LocalVar v) v.var_type |
|
694 |
with Not_found -> |
|
695 |
try (* id is a constant *) |
|
696 |
let c = Corelang.var_decl_of_const (const_of_top (Hashtbl.find Corelang.consts_table id)) |
|
697 |
in mk_val (LocalVar c) c.var_type |
|
698 |
with Not_found -> |
|
699 |
(* id is a tag *) |
|
700 |
let t = Const_tag id |
|
701 |
in mk_val (Cst t) (Typing.type_const loc t) |
|
702 |
|
|
703 |
(* type of internal fun used in dimension expression *) |
|
704 |
let type_of_value_appl f args = |
|
705 |
if List.mem f Basic_library.arith_funs |
|
706 |
then (List.hd args).value_type |
|
707 |
else Type_predef.type_bool |
|
708 |
|
|
709 |
let rec value_of_dimension m dim = |
|
710 |
match dim.Dimension.dim_desc with |
|
711 |
| Dimension.Dbool b -> |
|
712 |
mk_val (Cst (Const_tag (if b then Corelang.tag_true else Corelang.tag_false))) Type_predef.type_bool |
|
713 |
| Dimension.Dint i -> |
|
714 |
mk_val (Cst (Const_int i)) Type_predef.type_int |
|
715 |
| Dimension.Dident v -> value_of_ident dim.Dimension.dim_loc m v |
|
716 |
| Dimension.Dappl (f, args) -> |
|
717 |
let vargs = List.map (value_of_dimension m) args |
|
718 |
in mk_val (Fun (f, vargs)) (type_of_value_appl f vargs) |
|
719 |
| Dimension.Dite (i, t, e) -> |
|
720 |
(match List.map (value_of_dimension m) [i; t; e] with |
|
721 |
| [vi; vt; ve] -> mk_val (Fun ("ite", [vi; vt; ve])) vt.value_type |
|
722 |
| _ -> assert false) |
|
723 |
| Dimension.Dlink dim' -> value_of_dimension m dim' |
|
724 |
| _ -> assert false |
|
725 |
|
|
726 |
let rec dimension_of_value value = |
|
727 |
match value.value_desc with |
|
728 |
| Cst (Const_tag t) when t = Corelang.tag_true -> Dimension.mkdim_bool Location.dummy_loc true |
|
729 |
| Cst (Const_tag t) when t = Corelang.tag_false -> Dimension.mkdim_bool Location.dummy_loc false |
|
730 |
| Cst (Const_int i) -> Dimension.mkdim_int Location.dummy_loc i |
|
731 |
| LocalVar v -> Dimension.mkdim_ident Location.dummy_loc v.var_id |
|
732 |
| Fun (f, args) -> Dimension.mkdim_appl Location.dummy_loc f (List.map dimension_of_value args) |
|
733 |
| _ -> assert false |
|
734 | 381 |
|
735 | 382 |
(* Local Variables: *) |
736 | 383 |
(* compile-command:"make -C .." *) |
Also available in: Unified diff
Further restructuring:
- arrow.ml* to define basic builder for arrow (node, name, ...)
- machine_code_common similar to corelang but for machine_code (printers, some builders, ...)
- machine_code restricted to the translatation from normalized nodes to machines