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