Project

General

Profile

Download (16 KB) Statistics
| Branch: | Tag: | Revision:
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
type aut_state = {
17
  incoming_r' : var_decl;
18
  incoming_s' : var_decl;
19
  incoming_r : var_decl;
20
  incoming_s : var_decl;
21
  actual_r : var_decl;
22
  actual_s : var_decl;
23
}
24

    
25
let as_clock var_decl =
26
  let tydec = var_decl.var_dec_type in
27
  {
28
    var_decl with
29
    var_dec_type =
30
      {
31
        ty_dec_desc = Tydec_clock tydec.ty_dec_desc;
32
        ty_dec_loc = tydec.ty_dec_loc;
33
      };
34
  }
35

    
36
let mkbool loc b = mkexpr loc (Expr_const (const_of_bool b))
37

    
38
let mkident loc id = mkexpr loc (Expr_ident id)
39

    
40
let mkconst loc id = mkexpr loc (Expr_const (Const_tag id))
41

    
42
let mkfby loc e1 e2 = mkexpr loc (Expr_arrow (e1, mkexpr loc (Expr_pre e2)))
43

    
44
let mkpair loc e1 e2 = 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
51
    (Expr_ite
52
       ( expr,
53
         mkexpr loc (Expr_tuple [ mkbool loc restart; mkident loc st ]),
54
         cont ))
55

    
56
let mkhandler loc st unless until locals (stmts, asserts, annots) =
57
  {
58
    hand_state = st;
59
    hand_unless = unless;
60
    hand_until = until;
61
    hand_locals = locals;
62
    hand_stmts = stmts;
63
    hand_asserts = asserts;
64
    hand_annots = annots;
65
    hand_loc = loc;
66
  }
67

    
68
let mkautomata loc id handlers =
69
  { aut_id = id; aut_handlers = handlers; aut_loc = loc }
70

    
71
let expr_of_exit loc restart state conds tag =
72
  mkexpr loc
73
    (Expr_when
74
       ( List.fold_right add_branch conds (mkidentpair loc restart state),
75
         state,
76
         tag ))
77

    
78
let unless_read reads handler =
79
  let res =
80
    List.fold_left
81
      (fun read (_, c, _, _) -> Utils.ISet.union read (get_expr_vars c))
82
      reads handler.hand_unless
83
  in
84
  (* Format.eprintf "unless_reads %s = %a@." handler.hand_state (fprintf_list
85
     ~sep:" , " (fun fmt v -> Format.fprintf fmt "%s" v)) (ISet.elements reads);
86
     Format.eprintf "unless_reads' %s = %a@." handler.hand_state (fprintf_list
87
     ~sep:" , " (fun fmt v -> Format.fprintf fmt "%s" v)) (ISet.elements res); *)
88
  res
89

    
90
let until_read reads handler =
91
  List.fold_left
92
    (fun read (_, c, _, _) -> Utils.ISet.union read (get_expr_vars c))
93
    reads handler.hand_until
94

    
95
let rec handler_read reads handler =
96
  let locals =
97
    List.fold_left
98
      (fun locals v -> ISet.add v.var_id locals)
99
      ISet.empty handler.hand_locals
100
  in
101
  let allvars =
102
    List.fold_left
103
      (fun read stmt ->
104
        match stmt with
105
        | Eq eq ->
106
          Utils.ISet.union read (get_expr_vars eq.eq_rhs)
107
        | Aut aut ->
108
          automata_read read aut)
109
      reads handler.hand_stmts
110
  in
111
  let res = ISet.diff allvars locals in
112
  (* Format.eprintf "handler_allvars %s = %a@." handler.hand_state (fprintf_list
113
     ~sep:" , " (fun fmt v -> Format.fprintf fmt "%s" v)) (ISet.elements
114
     allvars); Format.eprintf "handler_read %s = %a@." handler.hand_state
115
     (fprintf_list ~sep:" , " (fun fmt v -> Format.fprintf fmt "%s" v))
116
     (ISet.elements res); *)
117
  res
118

    
119
and automata_read reads aut =
120
  List.fold_left
121
    (fun read handler ->
122
      until_read (handler_read (unless_read read handler) handler) handler)
123
    reads aut.aut_handlers
124

    
125
let rec handler_write writes handler =
126
  let locals =
127
    List.fold_left
128
      (fun locals v -> ISet.add v.var_id locals)
129
      ISet.empty handler.hand_locals
130
  in
131
  let allvars =
132
    List.fold_left
133
      (fun write stmt ->
134
        match stmt with
135
        | Eq eq ->
136
          List.fold_left (fun write v -> ISet.add v write) write eq.eq_lhs
137
        | Aut aut ->
138
          List.fold_left handler_write write aut.aut_handlers)
139
      writes handler.hand_stmts
140
  in
141
  ISet.diff allvars locals
142

    
143
let node_vars_of_idents node iset =
144
  List.fold_right
145
    (fun v res -> if ISet.mem v.var_id iset then v :: res else res)
146
    (get_node_vars node) []
147

    
148
let mkautomata_state nodeid used typedef loc id =
149
  let tydec_bool = { ty_dec_desc = Tydec_bool; ty_dec_loc = loc } in
150
  let tydec_state id = { ty_dec_desc = Tydec_const id; ty_dec_loc = loc } in
151
  let ckdec_any = { ck_dec_desc = Ckdec_any; ck_dec_loc = loc } in
152
  let incoming_r' = mk_new_name used (id ^ "__next_restart_in") in
153
  let incoming_s' = mk_new_name used (id ^ "__next_state_in") in
154
  let incoming_r = mk_new_name used (id ^ "__restart_in") in
155
  let incoming_s = mk_new_name used (id ^ "__state_in") in
156
  let actual_r = mk_new_name used (id ^ "__restart_act") in
157
  let actual_s = mk_new_name used (id ^ "__state_act") in
158
  {
159
    incoming_r' =
160
      mkvar_decl loc
161
        (incoming_r', tydec_bool, ckdec_any, false, None, Some nodeid);
162
    incoming_s' =
163
      mkvar_decl loc
164
        ( incoming_s',
165
          tydec_state typedef.tydef_id,
166
          ckdec_any,
167
          false,
168
          None,
169
          Some nodeid );
170
    incoming_r =
171
      mkvar_decl loc
172
        (incoming_r, tydec_bool, ckdec_any, false, None, Some nodeid);
173
    incoming_s =
174
      mkvar_decl loc
175
        ( incoming_s,
176
          tydec_state typedef.tydef_id,
177
          ckdec_any,
178
          false,
179
          None,
180
          Some nodeid );
181
    actual_r =
182
      mkvar_decl loc (actual_r, tydec_bool, ckdec_any, false, None, Some nodeid);
183
    actual_s =
184
      mkvar_decl loc
185
        ( actual_s,
186
          tydec_state typedef.tydef_id,
187
          ckdec_any,
188
          false,
189
          None,
190
          Some nodeid );
191
  }
192

    
193
let vars_of_aut_state aut_state =
194
  [
195
    aut_state.incoming_r';
196
    aut_state.incoming_r;
197
    aut_state.actual_r;
198
    aut_state.incoming_s';
199
    as_clock aut_state.incoming_s;
200
    as_clock aut_state.actual_s;
201
  ]
202

    
203
let node_of_unless nused node aut_id aut_state handler =
204
  (*Format.eprintf "node_of_unless %s@." node.node_id;*)
205
  let inputs = unless_read ISet.empty handler in
206
  let var_inputs =
207
    aut_state.incoming_r
208
    (*:: aut_state.incoming_s*)
209
    :: node_vars_of_idents node inputs
210
  in
211
  let var_outputs = [ aut_state.actual_r; aut_state.actual_s ] in
212
  let init_expr =
213
    mkpair handler.hand_loc
214
      (mkident handler.hand_loc aut_state.incoming_r.var_id)
215
      (mkconst handler.hand_loc handler.hand_state)
216
  in
217
  (* let init_expr = mkidentpair handler.hand_loc aut_state.incoming_r.var_id
218
     aut_state.incoming_s.var_id in *)
219
  let expr_outputs = List.fold_right add_branch handler.hand_unless init_expr in
220
  let eq_outputs =
221
    Eq
222
      (mkeq handler.hand_loc
223
         ([ aut_state.actual_r.var_id; aut_state.actual_s.var_id ], expr_outputs))
224
  in
225
  let node_id =
226
    mk_new_name nused (Format.sprintf "%s__%s_unless" aut_id handler.hand_state)
227
  in
228
  let args =
229
    List.map
230
      (fun v ->
231
        mkexpr handler.hand_loc
232
          (Expr_when
233
             ( mkident handler.hand_loc v.var_id,
234
               aut_state.incoming_s.var_id,
235
               handler.hand_state )))
236
      var_inputs
237
  in
238
  let reset = Some (mkident handler.hand_loc aut_state.incoming_r.var_id) in
239
  ( {
240
      node_id;
241
      node_type = Types.new_var ();
242
      node_clock = Clocks.new_var true;
243
      node_inputs = List.map copy_var_decl var_inputs;
244
      node_outputs = List.map copy_var_decl var_outputs;
245
      node_locals = [];
246
      node_gencalls = [];
247
      node_checks = [];
248
      node_asserts = [];
249
      node_stmts = [ eq_outputs ];
250
      node_dec_stateless = false;
251
      node_stateless = None;
252
      node_spec = None;
253
      node_annot = [];
254
      node_iscontract = false;
255
    },
256
    mkexpr handler.hand_loc
257
      (Expr_appl (node_id, mkexpr handler.hand_loc (Expr_tuple args), reset)) )
258

    
259
let rename_output used name = mk_new_name used (Format.sprintf "%s_out" name)
260

    
261
let rec rename_stmts_outputs frename stmts =
262
  match stmts with
263
  | [] ->
264
    []
265
  | Eq eq :: q ->
266
    let eq' = Eq { eq with eq_lhs = List.map frename eq.eq_lhs } in
267
    eq' :: rename_stmts_outputs frename q
268
  | Aut aut :: q ->
269
    let handlers' =
270
      List.map
271
        (fun h ->
272
          { h with hand_stmts = rename_stmts_outputs frename h.hand_stmts })
273
        aut.aut_handlers
274
    in
275
    let aut' = Aut { aut with aut_handlers = handlers' } in
276
    aut' :: rename_stmts_outputs frename q
277

    
278
let mk_frename used outputs =
279
  let table =
280
    ISet.fold
281
      (fun name table -> IMap.add name (rename_output used name) table)
282
      outputs IMap.empty
283
  in
284
  fun name -> try IMap.find name table with Not_found -> name
285

    
286
let node_of_assign_until nused used node aut_id aut_state handler =
287
  (*Format.eprintf "node_of_assign_until %s@." node.node_id;*)
288
  let writes = handler_write ISet.empty handler in
289
  let inputs =
290
    ISet.diff (handler_read (until_read ISet.empty handler) handler) writes
291
  in
292
  let frename = mk_frename used writes in
293
  let var_inputs =
294
    aut_state.actual_r
295
    (*:: aut_state.actual_s*)
296
    :: node_vars_of_idents node inputs
297
  in
298
  let new_var_locals = node_vars_of_idents node writes in
299
  let var_outputs =
300
    List.sort IdentModule.compare (node_vars_of_idents node writes)
301
  in
302
  let new_var_outputs =
303
    List.map
304
      (fun vdecl -> { vdecl with var_id = frename vdecl.var_id })
305
      var_outputs
306
  in
307
  let new_output_eqs =
308
    List.map2
309
      (fun o o' ->
310
        Eq
311
          (mkeq handler.hand_loc
312
             ([ o'.var_id ], mkident handler.hand_loc o.var_id)))
313
      var_outputs new_var_outputs
314
  in
315
  let init_until =
316
    mkpair handler.hand_loc
317
      (mkconst handler.hand_loc tag_false)
318
      (mkconst handler.hand_loc handler.hand_state)
319
  in
320
  let until_expr = List.fold_right add_branch handler.hand_until init_until in
321
  let until_eq =
322
    Eq
323
      (mkeq handler.hand_loc
324
         ( [ aut_state.incoming_r.var_id; aut_state.incoming_s.var_id ],
325
           until_expr ))
326
  in
327
  let node_id =
328
    mk_new_name nused
329
      (Format.sprintf "%s__%s_handler_until" aut_id handler.hand_state)
330
  in
331
  let args =
332
    List.map
333
      (fun v ->
334
        mkexpr handler.hand_loc
335
          (Expr_when
336
             ( mkident handler.hand_loc v.var_id,
337
               aut_state.actual_s.var_id,
338
               handler.hand_state )))
339
      var_inputs
340
  in
341
  let reset = Some (mkident handler.hand_loc aut_state.actual_r.var_id) in
342
  ( List.fold_left (fun res v -> ISet.add v.var_id res) ISet.empty var_outputs,
343
    {
344
      node_id;
345
      node_type = Types.new_var ();
346
      node_clock = Clocks.new_var true;
347
      node_inputs = List.map copy_var_decl var_inputs;
348
      node_outputs =
349
        List.map copy_var_decl
350
          (aut_state.incoming_r :: aut_state.incoming_s :: new_var_outputs);
351
      node_locals = List.map copy_var_decl (new_var_locals @ handler.hand_locals);
352
      node_gencalls = [];
353
      node_checks = [];
354
      node_asserts = handler.hand_asserts;
355
      node_stmts = until_eq :: new_output_eqs @ handler.hand_stmts;
356
      node_dec_stateless = false;
357
      node_stateless = None;
358
      node_spec = None;
359
      node_annot = handler.hand_annots;
360
      node_iscontract = false;
361
    },
362
    mkexpr handler.hand_loc
363
      (Expr_appl (node_id, mkexpr handler.hand_loc (Expr_tuple args), reset)) )
364

    
365
let typedef_of_automata aut =
366
  let tname = Format.sprintf "%s__type" aut.aut_id in
367
  {
368
    tydef_id = tname;
369
    tydef_desc = Tydec_enum (List.map (fun h -> h.hand_state) aut.aut_handlers);
370
  }
371

    
372
let expand_automata nused used owner typedef node aut =
373
  let initial = (List.hd aut.aut_handlers).hand_state in
374
  let aut_state =
375
    mkautomata_state node.node_id used typedef aut.aut_loc aut.aut_id
376
  in
377
  let unodes =
378
    List.map
379
      (fun h -> node_of_unless nused node aut.aut_id aut_state h)
380
      aut.aut_handlers
381
  in
382
  let aunodes =
383
    List.map
384
      (fun h -> node_of_assign_until nused used node aut.aut_id aut_state h)
385
      aut.aut_handlers
386
  in
387
  let all_outputs =
388
    List.fold_left
389
      (fun all (outputs, _, _) -> ISet.union outputs all)
390
      ISet.empty aunodes
391
  in
392
  let unless_handlers =
393
    List.map2 (fun h (_, c) -> h.hand_state, c) aut.aut_handlers unodes
394
  in
395
  let unless_expr =
396
    mkexpr aut.aut_loc
397
      (Expr_merge (aut_state.incoming_s.var_id, unless_handlers))
398
  in
399
  let unless_eq =
400
    mkeq aut.aut_loc
401
      ([ aut_state.actual_r.var_id; aut_state.actual_s.var_id ], unless_expr)
402
  in
403
  let assign_until_handlers =
404
    List.map2 (fun h (_, _, c) -> h.hand_state, c) aut.aut_handlers aunodes
405
  in
406
  let assign_until_expr =
407
    mkexpr aut.aut_loc
408
      (Expr_merge (aut_state.actual_s.var_id, assign_until_handlers))
409
  in
410
  let assign_until_vars =
411
    [ aut_state.incoming_r'.var_id; aut_state.incoming_s'.var_id ]
412
    @ ISet.elements all_outputs
413
  in
414
  let assign_until_eq =
415
    mkeq aut.aut_loc (assign_until_vars, assign_until_expr)
416
  in
417
  let fby_incoming_expr =
418
    mkfby aut.aut_loc
419
      (mkpair aut.aut_loc
420
         (mkconst aut.aut_loc tag_false)
421
         (mkconst aut.aut_loc initial))
422
      (mkidentpair aut.aut_loc aut_state.incoming_r'.var_id
423
         aut_state.incoming_s'.var_id)
424
  in
425
  let incoming_eq =
426
    mkeq aut.aut_loc
427
      ( [ aut_state.incoming_r.var_id; aut_state.incoming_s.var_id ],
428
        fby_incoming_expr )
429
  in
430
  let locals' = vars_of_aut_state aut_state in
431
  let eqs' = [ Eq unless_eq; Eq assign_until_eq; Eq incoming_eq ] in
432
  ( List.map2
433
      (fun h (n, _) -> mktop_decl h.hand_loc owner false (Node n))
434
      aut.aut_handlers unodes
435
    @ List.map2
436
        (fun h (_, n, _) -> mktop_decl h.hand_loc owner false (Node n))
437
        aut.aut_handlers aunodes,
438
    locals',
439
    eqs' )
440

    
441
let expand_node_stmt nused used owner node (top_types, top_nodes, locals, eqs)
442
    stmt =
443
  match stmt with
444
  | Eq eq ->
445
    top_types, top_nodes, locals, Eq eq :: eqs
446
  | Aut aut ->
447
    let typedef = typedef_of_automata aut in
448
    let used' name =
449
      used name || List.exists (fun v -> v.var_id = name) locals
450
    in
451
    let nused' name =
452
      nused name
453
      || List.exists
454
           (fun t ->
455
             match t.top_decl_desc with
456
             | ImportedNode nd ->
457
               nd.nodei_id = name
458
             | Node nd ->
459
               nd.node_id = name
460
             | _ ->
461
               false)
462
           top_nodes
463
    in
464
    let top_decls', locals', eqs' =
465
      expand_automata nused' used' owner typedef node aut
466
    in
467
    let top_typedef = mktop_decl aut.aut_loc owner false (TypeDef typedef) in
468
    ( top_typedef :: top_types,
469
      top_decls' @ top_nodes,
470
      locals' @ locals,
471
      eqs' @ eqs )
472

    
473
let expand_node_stmts nused used loc owner node =
474
  let top_types', top_nodes', locals', eqs' =
475
    List.fold_left
476
      (expand_node_stmt nused used owner node)
477
      ([], [], [], []) node.node_stmts
478
  in
479
  let node' =
480
    { node with node_locals = locals' @ node.node_locals; node_stmts = eqs' }
481
  in
482
  let top_node = mktop_decl loc owner false (Node node') in
483
  top_types', top_node, top_nodes'
484

    
485
let rec expand_decls_rec nused top_decls =
486
  match top_decls with
487
  | [] ->
488
    []
489
  | top_decl :: q -> (
490
    match top_decl.top_decl_desc with
491
    | Node nd ->
492
      let used name =
493
        List.exists (fun v -> v.var_id = name) nd.node_inputs
494
        || List.exists (fun v -> v.var_id = name) nd.node_outputs
495
        || List.exists (fun v -> v.var_id = name) nd.node_locals
496
      in
497
      let top_types', top_decl', top_nodes' =
498
        expand_node_stmts nused used top_decl.top_decl_loc
499
          top_decl.top_decl_owner nd
500
      in
501
      top_types' @ top_decl' :: expand_decls_rec nused (top_nodes' @ q)
502
    | _ ->
503
      top_decl :: expand_decls_rec nused q)
504

    
505
let expand_decls top_decls =
506
  let top_names =
507
    List.fold_left
508
      (fun names t ->
509
        match t.top_decl_desc with
510
        | Node nd ->
511
          ISet.add nd.node_id names
512
        | ImportedNode nd ->
513
          ISet.add nd.nodei_id names
514
        | _ ->
515
          names)
516
      ISet.empty top_decls
517
  in
518
  let nused name = ISet.mem name top_names in
519
  expand_decls_rec nused top_decls
520

    
521
(* Local Variables: *)
522
(* compile-command:"make -C .." *)
523
(* End: *)
(7-7/66)