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