lustrec / src / automata.ml @ 4f26dcf5
History | View | Annotate | Download (14.7 KB)
1 |
(********************************************************************) |
---|---|
2 |
(* *) |
3 |
(* The LustreC compiler toolset / The LustreC Development Team *) |
4 |
(* Copyright 2012 - -- ONERA - CNRS - INPT *) |
5 |
(* *) |
6 |
(* LustreC is free software, distributed WITHOUT ANY WARRANTY *) |
7 |
(* under the terms of the GNU Lesser General Public License *) |
8 |
(* version 2.1. *) |
9 |
(* *) |
10 |
(********************************************************************) |
11 |
|
12 |
open Utils |
13 |
open Lustre_types |
14 |
open Corelang |
15 |
|
16 |
|
17 |
type aut_state = |
18 |
{ |
19 |
incoming_r' : var_decl; |
20 |
incoming_s' : var_decl; |
21 |
incoming_r : var_decl; |
22 |
incoming_s : var_decl; |
23 |
actual_r : var_decl; |
24 |
actual_s : var_decl |
25 |
} |
26 |
|
27 |
let as_clock var_decl = |
28 |
let tydec = var_decl.var_dec_type in |
29 |
{ var_decl with var_dec_type = { ty_dec_desc = Tydec_clock tydec.ty_dec_desc; ty_dec_loc = tydec.ty_dec_loc } } |
30 |
|
31 |
let mkbool loc b = |
32 |
mkexpr loc (Expr_const (const_of_bool b)) |
33 |
|
34 |
let mkident loc id = |
35 |
mkexpr loc (Expr_ident id) |
36 |
|
37 |
let mkconst loc id = |
38 |
mkexpr loc (Expr_const (Const_tag id)) |
39 |
|
40 |
let mkfby loc e1 e2 = |
41 |
mkexpr loc (Expr_arrow (e1, mkexpr loc (Expr_pre e2))) |
42 |
|
43 |
let mkpair loc e1 e2 = |
44 |
mkexpr loc (Expr_tuple [e1; e2]) |
45 |
|
46 |
let mkidentpair loc restart state = |
47 |
mkexpr loc (Expr_tuple [mkident loc restart; mkident loc state]) |
48 |
|
49 |
let add_branch (loc, expr, restart, st) cont = |
50 |
mkexpr loc (Expr_ite (expr, mkexpr loc (Expr_tuple [mkbool loc restart; mkident loc st]), cont)) |
51 |
|
52 |
let mkhandler loc st unless until locals (stmts, asserts, annots) = |
53 |
{hand_state = st; |
54 |
hand_unless = unless; |
55 |
hand_until = until; |
56 |
hand_locals = locals; |
57 |
hand_stmts = stmts; |
58 |
hand_asserts = asserts; |
59 |
hand_annots = annots; |
60 |
hand_loc = loc} |
61 |
|
62 |
let mkautomata loc id handlers = |
63 |
{aut_id = id; |
64 |
aut_handlers = handlers; |
65 |
aut_loc = loc} |
66 |
|
67 |
let expr_of_exit loc restart state conds tag = |
68 |
mkexpr loc (Expr_when (List.fold_right add_branch conds (mkidentpair loc restart state), state, tag)) |
69 |
|
70 |
let rec unless_read reads handler = |
71 |
let res = |
72 |
List.fold_left (fun read (_, c, _, _) -> Utils.ISet.union read (get_expr_vars c)) reads handler.hand_unless |
73 |
in |
74 |
( |
75 |
(* |
76 |
Format.eprintf "unless_reads %s = %a@." handler.hand_state (fprintf_list ~sep:" , " (fun fmt v -> Format.fprintf fmt "%s" v)) (ISet.elements reads); |
77 |
Format.eprintf "unless_reads' %s = %a@." handler.hand_state (fprintf_list ~sep:" , " (fun fmt v -> Format.fprintf fmt "%s" v)) (ISet.elements res); |
78 |
*) |
79 |
res |
80 |
) |
81 |
|
82 |
let rec until_read reads handler = |
83 |
List.fold_left (fun read (_, c, _, _) -> Utils.ISet.union read (get_expr_vars c)) reads handler.hand_until |
84 |
|
85 |
let rec handler_read reads handler = |
86 |
let locals = List.fold_left (fun locals v -> ISet.add v.var_id locals) ISet.empty handler.hand_locals in |
87 |
let allvars = |
88 |
List.fold_left (fun read stmt -> |
89 |
match stmt with |
90 |
| Eq eq -> Utils.ISet.union read (get_expr_vars eq.eq_rhs) |
91 |
| Aut aut -> automata_read read aut) reads handler.hand_stmts |
92 |
in let res = ISet.diff allvars locals |
93 |
in |
94 |
( |
95 |
(* |
96 |
Format.eprintf "handler_allvars %s = %a@." handler.hand_state (fprintf_list ~sep:" , " (fun fmt v -> Format.fprintf fmt "%s" v)) (ISet.elements allvars); |
97 |
Format.eprintf "handler_read %s = %a@." handler.hand_state (fprintf_list ~sep:" , " (fun fmt v -> Format.fprintf fmt "%s" v)) (ISet.elements res); |
98 |
*) |
99 |
res |
100 |
) |
101 |
|
102 |
and automata_read reads aut = |
103 |
List.fold_left (fun read handler -> until_read (handler_read (unless_read read handler) handler) handler) reads aut.aut_handlers |
104 |
|
105 |
let rec handler_write writes handler = |
106 |
let locals = List.fold_left (fun locals v -> ISet.add v.var_id locals) ISet.empty handler.hand_locals in |
107 |
let allvars = |
108 |
List.fold_left (fun write stmt -> |
109 |
match stmt with |
110 |
| Eq eq -> List.fold_left (fun write v -> ISet.add v write) write eq.eq_lhs |
111 |
| Aut aut -> List.fold_left handler_write write aut.aut_handlers) writes handler.hand_stmts |
112 |
in ISet.diff allvars locals |
113 |
|
114 |
let node_vars_of_idents node iset = |
115 |
List.fold_right (fun v res -> if ISet.mem v.var_id iset then v :: res else res) (get_node_vars node) [] |
116 |
|
117 |
let mkautomata_state nodeid used typedef loc id = |
118 |
let tydec_bool = { ty_dec_desc = Tydec_bool; ty_dec_loc = loc } in |
119 |
let tydec_state id = { ty_dec_desc = Tydec_const id; ty_dec_loc = loc } in |
120 |
let ckdec_any = { ck_dec_desc = Ckdec_any; ck_dec_loc = loc } in |
121 |
let incoming_r' = mk_new_name used (id ^ "__next_restart_in") in |
122 |
let incoming_s' = mk_new_name used (id ^ "__next_state_in") in |
123 |
let incoming_r = mk_new_name used (id ^ "__restart_in") in |
124 |
let incoming_s = mk_new_name used (id ^ "__state_in") in |
125 |
let actual_r = mk_new_name used (id ^ "__restart_act") in |
126 |
let actual_s = mk_new_name used (id ^ "__state_act") in |
127 |
{ |
128 |
incoming_r' = mkvar_decl loc (incoming_r', tydec_bool, ckdec_any, false, None, Some nodeid); |
129 |
incoming_s' = mkvar_decl loc (incoming_s', tydec_state typedef.tydef_id, ckdec_any, false, None, Some nodeid); |
130 |
incoming_r = mkvar_decl loc (incoming_r, tydec_bool, ckdec_any, false, None, Some nodeid); |
131 |
incoming_s = mkvar_decl loc (incoming_s, tydec_state typedef.tydef_id, ckdec_any, false, None, Some nodeid); |
132 |
actual_r = mkvar_decl loc (actual_r , tydec_bool, ckdec_any, false, None, Some nodeid); |
133 |
actual_s = mkvar_decl loc (actual_s , tydec_state typedef.tydef_id, ckdec_any, false, None, Some nodeid) |
134 |
} |
135 |
|
136 |
let vars_of_aut_state aut_state = |
137 |
[aut_state.incoming_r'; aut_state.incoming_r; aut_state.actual_r; aut_state.incoming_s'; as_clock aut_state.incoming_s; as_clock aut_state.actual_s] |
138 |
|
139 |
let node_of_unless nused used node aut_id aut_state handler = |
140 |
(*Format.eprintf "node_of_unless %s@." node.node_id;*) |
141 |
let inputs = unless_read ISet.empty handler in |
142 |
let var_inputs = aut_state.incoming_r (*:: aut_state.incoming_s*) :: (node_vars_of_idents node inputs) in |
143 |
let var_outputs = aut_state.actual_r :: aut_state.actual_s :: [] in |
144 |
let init_expr = mkpair handler.hand_loc (mkident handler.hand_loc aut_state.incoming_r.var_id) (mkconst handler.hand_loc handler.hand_state) in |
145 |
(* let init_expr = mkidentpair handler.hand_loc aut_state.incoming_r.var_id aut_state.incoming_s.var_id in *) |
146 |
let expr_outputs = List.fold_right add_branch handler.hand_unless init_expr in |
147 |
let eq_outputs = Eq (mkeq handler.hand_loc ([aut_state.actual_r.var_id; aut_state.actual_s.var_id], expr_outputs)) in |
148 |
let node_id = mk_new_name nused (Format.sprintf "%s__%s_unless" aut_id handler.hand_state) in |
149 |
let args = List.map (fun v -> mkexpr handler.hand_loc (Expr_when (mkident handler.hand_loc v.var_id, aut_state.incoming_s.var_id, handler.hand_state))) var_inputs in |
150 |
let reset = Some (mkident handler.hand_loc aut_state.incoming_r.var_id) in |
151 |
{ |
152 |
node_id = node_id; |
153 |
node_type = Types.new_var (); |
154 |
node_clock = Clocks.new_var true; |
155 |
node_inputs = List.map copy_var_decl var_inputs; |
156 |
node_outputs = List.map copy_var_decl var_outputs; |
157 |
node_locals = []; |
158 |
node_gencalls = []; |
159 |
node_checks = []; |
160 |
node_asserts = []; |
161 |
node_stmts = [ eq_outputs ]; |
162 |
node_dec_stateless = false; |
163 |
node_stateless = None; |
164 |
node_spec = None; |
165 |
node_annot = [] |
166 |
}, |
167 |
mkexpr handler.hand_loc (Expr_appl (node_id, mkexpr handler.hand_loc (Expr_tuple args), reset)) |
168 |
|
169 |
|
170 |
let rename_output used name = mk_new_name used (Format.sprintf "%s_out" name) |
171 |
|
172 |
let rec rename_stmts_outputs frename stmts = |
173 |
match stmts with |
174 |
| [] -> [] |
175 |
| (Eq eq) :: q -> let eq' = Eq { eq with eq_lhs = List.map frename eq.eq_lhs } in |
176 |
eq' :: rename_stmts_outputs frename q |
177 |
| (Aut aut) :: q -> let handlers' = List.map (fun h -> { h with hand_stmts = rename_stmts_outputs frename h.hand_stmts}) aut.aut_handlers in |
178 |
let aut' = Aut { aut with aut_handlers = handlers' } in |
179 |
aut' :: rename_stmts_outputs frename q |
180 |
|
181 |
let mk_frename used outputs = |
182 |
let table = ISet.fold (fun name table -> IMap.add name (rename_output used name) table) outputs IMap.empty in |
183 |
(fun name -> try IMap.find name table with Not_found -> name) |
184 |
|
185 |
let node_of_assign_until nused used node aut_id aut_state handler = |
186 |
(*Format.eprintf "node_of_assign_until %s@." node.node_id;*) |
187 |
let writes = handler_write ISet.empty handler in |
188 |
let inputs = ISet.diff (handler_read (until_read ISet.empty handler) handler) writes in |
189 |
let frename = mk_frename used writes in |
190 |
let var_inputs = aut_state.actual_r (*:: aut_state.actual_s*) :: node_vars_of_idents node inputs in |
191 |
let new_var_locals = node_vars_of_idents node writes in |
192 |
let var_outputs = List.sort IdentModule.compare (node_vars_of_idents node writes) in |
193 |
let new_var_outputs = List.map (fun vdecl -> { vdecl with var_id = frename vdecl.var_id }) var_outputs in |
194 |
let new_output_eqs = List.map2 (fun o o' -> Eq (mkeq handler.hand_loc ([o'.var_id], mkident handler.hand_loc o.var_id))) var_outputs new_var_outputs in |
195 |
let init_until = mkpair handler.hand_loc (mkconst handler.hand_loc tag_false) (mkconst handler.hand_loc handler.hand_state) in |
196 |
let until_expr = List.fold_right add_branch handler.hand_until init_until in |
197 |
let until_eq = Eq (mkeq handler.hand_loc ([aut_state.incoming_r.var_id; aut_state.incoming_s.var_id], until_expr)) in |
198 |
let node_id = mk_new_name nused (Format.sprintf "%s__%s_handler_until" aut_id handler.hand_state) in |
199 |
let args = List.map (fun v -> mkexpr handler.hand_loc (Expr_when (mkident handler.hand_loc v.var_id, aut_state.actual_s.var_id, handler.hand_state))) var_inputs in |
200 |
let reset = Some (mkident handler.hand_loc aut_state.actual_r.var_id) in |
201 |
List.fold_left (fun res v -> ISet.add v.var_id res) ISet.empty var_outputs, |
202 |
{ |
203 |
node_id = node_id; |
204 |
node_type = Types.new_var (); |
205 |
node_clock = Clocks.new_var true; |
206 |
node_inputs = List.map copy_var_decl var_inputs; |
207 |
node_outputs = List.map copy_var_decl (aut_state.incoming_r :: aut_state.incoming_s :: new_var_outputs); |
208 |
node_locals = List.map copy_var_decl (new_var_locals @ handler.hand_locals); |
209 |
node_gencalls = []; |
210 |
node_checks = []; |
211 |
node_asserts = handler.hand_asserts; |
212 |
node_stmts = until_eq :: new_output_eqs @ handler.hand_stmts; |
213 |
node_dec_stateless = false; |
214 |
node_stateless = None; |
215 |
node_spec = None; |
216 |
node_annot = handler.hand_annots |
217 |
}, |
218 |
mkexpr handler.hand_loc (Expr_appl (node_id, mkexpr handler.hand_loc (Expr_tuple args), reset)) |
219 |
|
220 |
let typedef_of_automata aut = |
221 |
let tname = Format.sprintf "%s__type" aut.aut_id in |
222 |
{ tydef_id = tname; |
223 |
tydef_desc = Tydec_enum (List.map (fun h -> h.hand_state) aut.aut_handlers) |
224 |
} |
225 |
|
226 |
let expand_automata nused used owner typedef node aut = |
227 |
let initial = (List.hd aut.aut_handlers).hand_state in |
228 |
let aut_state = mkautomata_state node.node_id used typedef aut.aut_loc aut.aut_id in |
229 |
let unodes = List.map (fun h -> node_of_unless nused used node aut.aut_id aut_state h) aut.aut_handlers in |
230 |
let aunodes = List.map (fun h -> node_of_assign_until nused used node aut.aut_id aut_state h) aut.aut_handlers in |
231 |
let all_outputs = List.fold_left (fun all (outputs, _, _) -> ISet.union outputs all) ISet.empty aunodes in |
232 |
let unless_handlers = List.map2 (fun h (n, c) -> (h.hand_state, c)) aut.aut_handlers unodes in |
233 |
let unless_expr = mkexpr aut.aut_loc (Expr_merge (aut_state.incoming_s.var_id, unless_handlers)) in |
234 |
let unless_eq = mkeq aut.aut_loc ([aut_state.actual_r.var_id; aut_state.actual_s.var_id], unless_expr) in |
235 |
let assign_until_handlers = List.map2 (fun h (_, n, c) -> (h.hand_state, c)) aut.aut_handlers aunodes in |
236 |
let assign_until_expr = mkexpr aut.aut_loc (Expr_merge (aut_state.actual_s.var_id, assign_until_handlers)) in |
237 |
let assign_until_vars = [aut_state.incoming_r'.var_id; aut_state.incoming_s'.var_id] @ (ISet.elements all_outputs) in |
238 |
let assign_until_eq = mkeq aut.aut_loc (assign_until_vars, assign_until_expr) in |
239 |
let fby_incoming_expr = mkfby aut.aut_loc (mkpair aut.aut_loc (mkconst aut.aut_loc tag_false) (mkconst aut.aut_loc initial)) (mkidentpair aut.aut_loc aut_state.incoming_r'.var_id aut_state.incoming_s'.var_id) in |
240 |
let incoming_eq = mkeq aut.aut_loc ([aut_state.incoming_r.var_id; aut_state.incoming_s.var_id], fby_incoming_expr) in |
241 |
let locals' = vars_of_aut_state aut_state in |
242 |
let eqs' = [Eq unless_eq; Eq assign_until_eq; Eq incoming_eq] in |
243 |
( List.map2 (fun h (n, _) -> mktop_decl h.hand_loc owner false (Node n)) aut.aut_handlers unodes |
244 |
@ List.map2 (fun h (_, n, _) -> mktop_decl h.hand_loc owner false (Node n)) aut.aut_handlers aunodes, |
245 |
locals', |
246 |
eqs') |
247 |
|
248 |
let expand_node_stmt nused used owner node (top_types, top_nodes, locals, eqs) stmt = |
249 |
match stmt with |
250 |
| Eq eq -> (top_types, top_nodes, locals, (Eq eq)::eqs) |
251 |
| Aut aut -> |
252 |
let typedef = typedef_of_automata aut in |
253 |
let used' name = used name || List.exists (fun v -> v.var_id = name) locals in |
254 |
let nused' name = |
255 |
nused name || |
256 |
List.exists (fun t -> match t.top_decl_desc with |
257 |
| ImportedNode nd -> nd.nodei_id = name | Node nd -> nd.node_id = name |
258 |
| _ -> false) top_nodes in |
259 |
let (top_decls', locals', eqs') = expand_automata nused' used' owner typedef node aut in |
260 |
let top_typedef = mktop_decl aut.aut_loc owner false (TypeDef typedef) in |
261 |
(top_typedef :: top_types, top_decls'@top_nodes, locals'@locals, eqs'@eqs) |
262 |
|
263 |
let expand_node_stmts nused used loc owner node = |
264 |
let (top_types', top_nodes', locals', eqs') = |
265 |
List.fold_left (expand_node_stmt nused used owner node) ([], [], [], []) node.node_stmts in |
266 |
let node' = |
267 |
{ node with node_locals = locals'@node.node_locals; node_stmts = eqs' } in |
268 |
let top_node = mktop_decl loc owner false (Node node') in |
269 |
top_types', top_node, top_nodes' |
270 |
|
271 |
let rec expand_decls_rec nused top_decls = |
272 |
match top_decls with |
273 |
| [] -> [] |
274 |
| top_decl::q -> |
275 |
match top_decl.top_decl_desc with |
276 |
| Node nd -> |
277 |
let used name = |
278 |
List.exists (fun v -> v.var_id = name) nd.node_inputs |
279 |
|| List.exists (fun v -> v.var_id = name) nd.node_outputs |
280 |
|| List.exists (fun v -> v.var_id = name) nd.node_locals in |
281 |
let (top_types', top_decl', top_nodes') = expand_node_stmts nused used top_decl.top_decl_loc top_decl.top_decl_owner nd in |
282 |
top_types' @ (top_decl' :: expand_decls_rec nused (top_nodes'@q)) |
283 |
| _ -> top_decl :: expand_decls_rec nused q |
284 |
|
285 |
let expand_decls top_decls = |
286 |
let top_names = List.fold_left (fun names t -> match t.top_decl_desc with |
287 |
| Node nd -> ISet.add nd.node_id names |
288 |
| ImportedNode nd -> ISet.add nd.nodei_id names |
289 |
| _ -> names) ISet.empty top_decls in |
290 |
let nused name = ISet.mem name top_names in |
291 |
expand_decls_rec nused top_decls |
292 |
|
293 |
(* Local Variables: *) |
294 |
(* compile-command:"make -C .." *) |
295 |
(* End: *) |
296 |
|