Project

General

Profile

Download (16.4 KB) Statistics
| Branch: | Tag: | Revision:
1
open Lustre_types
2
open Machine_code_types
3
open Spec_types
4
open Corelang
5
open Utils.Format
6

    
7
let print_statelocaltag = true
8

    
9
let is_memory m id = List.exists (fun o -> o.var_id = id.var_id) m.mmemory
10

    
11
let is_reset_flag id = id.var_id = "_reset"
12

    
13
let pp_vdecl fmt v = pp_print_string fmt v.var_id
14

    
15
let rec pp_val m fmt v =
16
  let pp_val = pp_val m in
17
  match v.value_desc with
18
  | Cst c ->
19
    Printers.pp_const fmt c
20
  | Var v ->
21
    if is_memory m v then
22
      if print_statelocaltag then fprintf fmt "{%s}" v.var_id
23
      else pp_print_string fmt v.var_id
24
    else if print_statelocaltag then fprintf fmt "%s" v.var_id
25
    else pp_vdecl fmt v
26
  | Array vl ->
27
    pp_print_bracketed pp_val fmt vl
28
  | Access (t, i) ->
29
    fprintf fmt "%a[%a]" pp_val t pp_val i
30
  | Power (v, n) ->
31
    fprintf fmt "(%a^%a)" pp_val v pp_val n
32
  | Fun (n, vl) ->
33
    fprintf fmt "%s%a" n (pp_print_parenthesized pp_val) vl
34
  | ResetFlag ->
35
    fprintf fmt "RESET"
36

    
37
module PrintSpec = struct
38
  let pp_reg fmt = function
39
    | ResetFlag ->
40
      pp_print_string fmt "{RESET}"
41
    | StateVar v ->
42
      fprintf fmt "{OUT:%a}" pp_vdecl v
43

    
44
  let pp_expr :
45
      type a. machine_t -> formatter -> (value_t, a) expression_t -> unit =
46
   fun m fmt -> function
47
    | Val v ->
48
      pp_val m fmt v
49
    | Tag t ->
50
      pp_print_string fmt t
51
    | Var v ->
52
      pp_vdecl fmt v
53
    | Memory r ->
54
      pp_reg fmt r
55

    
56
  let pp_predicate m fmt p =
57
    let pp_expr : type a. formatter -> (value_t, a) expression_t -> unit =
58
     fun fmt e -> pp_expr m fmt e
59
    in
60
    match p with
61
    | Transition (f, inst, i, inputs, locals, outputs, _r, _mems, _insts) ->
62
      fprintf fmt "Transition_%a<%a>%a%a" pp_print_string f
63
        (pp_print_option
64
           ~none:(fun fmt () -> pp_print_string fmt "SELF")
65
           pp_print_string)
66
        inst
67
        (pp_print_option pp_print_int)
68
        i
69
        (pp_print_parenthesized pp_expr)
70
        (inputs @ locals @ outputs)
71
    | Reset (f, inst, r) ->
72
      fprintf fmt "Reset_%a<%a> on %a" pp_print_string f pp_print_string inst
73
        (pp_val m) r
74
    | MemoryPack (f, inst, i) ->
75
      fprintf fmt "MemoryPack_%a<%a>%a" pp_print_string f
76
        (pp_print_option
77
           ~none:(fun fmt () -> pp_print_string fmt "SELF")
78
           pp_print_string)
79
        inst
80
        (pp_print_option pp_print_int)
81
        i
82
    | ResetCleared f ->
83
      fprintf fmt "ResetCleared_%a" pp_print_string f
84
    | Initialization ->
85
      ()
86

    
87
  let pp_spec m =
88
    let pp_expr : type a. formatter -> (value_t, a) expression_t -> unit =
89
     fun fmt e -> pp_expr m fmt e
90
    in
91
    let rec pp_spec fmt f =
92
      match f with
93
      | True ->
94
        pp_print_string fmt "true"
95
      | False ->
96
        pp_print_string fmt "false"
97
      | Equal (a, b) ->
98
        fprintf fmt "%a == %a" pp_expr a pp_expr b
99
      | And fs ->
100
        pp_print_list
101
          ~pp_sep:(fun fmt () -> fprintf fmt "@ ∧ ")
102
          (fun fmt spec -> fprintf fmt "@[%a@]" pp_spec spec)
103
          fmt fs
104
      | Or fs ->
105
        pp_print_list
106
          ~pp_sep:(fun fmt () -> fprintf fmt "@ ∨ ")
107
          (fun fmt spec -> fprintf fmt "@[%a@]" pp_spec spec)
108
          fmt fs
109
      | Imply (a, b) ->
110
        fprintf fmt "%a@ -> %a" pp_spec a pp_spec b
111
      | Exists (xs, a) ->
112
        fprintf fmt "@[<hv 2>∃ @[<h>%a,@]@ %a@]"
113
          (pp_comma_list Printers.pp_var)
114
          xs pp_spec a
115
      | Forall (xs, a) ->
116
        fprintf fmt "@[<hv 2>∀ @[<h>%a,@]@ %a@]"
117
          (pp_comma_list Printers.pp_var)
118
          xs pp_spec a
119
      | Ternary (e, a, b) ->
120
        fprintf fmt "If %a Then (@[<hov>%a@]) Else (@[<hov>%a@])" pp_expr e
121
          pp_spec a pp_spec b
122
      | Predicate p ->
123
        pp_predicate m fmt p
124
      | StateVarPack r ->
125
        fprintf fmt "StateVarPack<%a>" pp_reg r
126
      | ExistsMem (_f, a, b) ->
127
        fprintf fmt "@[<hv 2>∃ MEM,@ %a@]" pp_spec (And [ a; b ])
128
    in
129
    pp_spec
130
end
131

    
132
let pp_spec m =
133
  if !Options.spec <> "no" then
134
    pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_prologue:pp_print_cut
135
      (fun fmt -> fprintf fmt "@[<h>--%@ %a@]" (PrintSpec.pp_spec m))
136
  else pp_print_nothing
137

    
138
let rec pp_instr m fmt i =
139
  let pp_val = pp_val m in
140
  let pp_branch = pp_branch m in
141
  (match i.instr_desc with
142
  | MLocalAssign (i, v) ->
143
    fprintf fmt "%s := %a" i.var_id pp_val v
144
  | MStateAssign (i, v) ->
145
    fprintf fmt "{%s} := %a" i.var_id pp_val v
146
  | MResetAssign b ->
147
    fprintf fmt "RESET := %a" pp_print_bool b
148
  | MSetReset i ->
149
    fprintf fmt "set_reset %s" i
150
  | MClearReset ->
151
    fprintf fmt "clear_reset %s" m.mname.node_id
152
  | MNoReset i ->
153
    fprintf fmt "noreset %s" i
154
  | MStep (il, i, vl) ->
155
    fprintf fmt "%a := %s%a" (pp_comma_list pp_vdecl) il i
156
      (pp_print_parenthesized pp_val)
157
      vl
158
  | MBranch (g, hl) ->
159
    fprintf fmt "@[<v 2>case(%a) {@,%a@]@,}" pp_val g
160
      (pp_print_list ~pp_open_box:pp_open_vbox0 pp_branch)
161
      hl
162
  | MComment s ->
163
    pp_print_string fmt s
164
  | MSpec s ->
165
    pp_print_string fmt ("@" ^ s));
166
  (* Annotation *)
167
  (* let _ = *)
168
  (* match i.lustre_expr with None -> () | Some e -> fprintf fmt " -- original
169
     expr: %a" Printers.pp_expr e *)
170
  (* in *)
171
  (match i.lustre_eq with
172
  | None ->
173
    ()
174
  | Some eq ->
175
    fprintf fmt " @[<h>-- original eq: %a@]" Printers.pp_node_eq eq);
176
  pp_spec m fmt i.instr_spec
177

    
178
and pp_branch m fmt (t, h) =
179
  fprintf fmt "@[<v 2>%s:@,%a@]" t
180
    (pp_print_list ~pp_open_box:pp_open_vbox0 (pp_instr m))
181
    h
182

    
183
let pp_instrs m = pp_print_list ~pp_open_box:pp_open_vbox0 (pp_instr m)
184

    
185
(* merge log: get_node_def was in c0f8 *)
186
(* Returns the node/machine associated to id in m calls *)
187
let get_node_def id m =
188
  try
189
    let decl, _ = List.assoc id m.mcalls in
190
    Corelang.node_of_top decl
191
  with Not_found ->
192
    (* eprintf "Unable to find node %s in list [%a]@.@?" *)
193
    (*   id *)
194
    (* (Utils.fprintf_list ~sep:", " (fun fmt (n,_) -> fprintf fmt "%s" n))
195
       m.mcalls *)
196
    (* ; *)
197
    raise Not_found
198

    
199
(* merge log: machine_vars was in 44686 *)
200
let machine_vars m =
201
  m.mstep.step_inputs @ m.mstep.step_locals @ m.mstep.step_outputs @ m.mmemory
202

    
203
let pp_step m fmt s =
204
  fprintf fmt
205
    "@[<v>inputs : %a@ outputs: %a@ locals : %a@ checks : %a@ instrs : @[%a@]@ \
206
     asserts : @[%a@]@]@ "
207
    (pp_comma_list Printers.pp_var)
208
    s.step_inputs
209
    (pp_comma_list Printers.pp_var)
210
    s.step_outputs
211
    (pp_comma_list Printers.pp_var)
212
    s.step_locals
213
    (pp_comma_list (fun fmt (_, c) -> pp_val m fmt c))
214
    s.step_checks (pp_instrs m) s.step_instrs
215
    (pp_comma_list (pp_val m))
216
    s.step_asserts
217

    
218
let pp_static_call fmt (node, args) =
219
  fprintf fmt "%s<%a>" (node_name node)
220
    (pp_comma_list Dimension.pp_dimension)
221
    args
222

    
223
let pp_instance fmt (o1, o2) = fprintf fmt "(%s, %a)" o1 pp_static_call o2
224

    
225
let pp_memory_pack m fmt mp =
226
  fprintf fmt "@[<v 2>MemoryPack_%a<SELF>%a =@ %a@]" pp_print_string
227
    mp.mpname.node_id
228
    (pp_print_option pp_print_int)
229
    mp.mpindex (PrintSpec.pp_spec m) mp.mpformula
230

    
231
let pp_memory_packs m fmt =
232
  if !Options.spec <> "no" then
233
    fprintf fmt "@[<v 2>memory_packs:@ %a@]" (pp_print_list (pp_memory_pack m))
234
  else pp_print_nothing fmt
235

    
236
let pp_transition m fmt t =
237
  fprintf fmt "@[<v 2>Transition_%a<SELF>%a%a =@ %a@]" pp_print_string
238
    t.tname.node_id
239
    (pp_print_option pp_print_int)
240
    t.tindex
241
    (pp_print_parenthesized pp_vdecl)
242
    (t.tinputs @ t.tlocals @ t.toutputs)
243
    (PrintSpec.pp_spec m) t.tformula
244

    
245
let pp_transitions m fmt =
246
  if !Options.spec <> "no" then
247
    fprintf fmt "@[<v 2>transitions:@ %a@]" (pp_print_list (pp_transition m))
248
  else pp_print_nothing fmt
249

    
250
let pp_machine fmt m =
251
  fprintf fmt
252
    "@[<v 2>machine %s@ mem      : %a@ instances: %a@ init     : %a@ const    \
253
     : %a@ step     :@   @[<v 2>%a@]@ spec     : @[<v>%t@ %a@ @ %a@]@ annot    \
254
     : @[%a@]@]@ "
255
    m.mname.node_id
256
    (pp_comma_list Printers.pp_var)
257
    m.mmemory
258
    (pp_comma_list pp_instance)
259
    m.minstances (pp_instrs m) m.minit (pp_instrs m) m.mconst (pp_step m)
260
    m.mstep
261
    (fun fmt ->
262
      match m.mspec.mnode_spec with
263
      | None ->
264
        ()
265
      | Some (NodeSpec id) ->
266
        fprintf fmt "cocospec: %s" id
267
      | Some (Contract spec) ->
268
        Printers.pp_spec fmt spec)
269
    (pp_memory_packs m) m.mspec.mmemory_packs (pp_transitions m)
270
    m.mspec.mtransitions
271
    (pp_print_list Printers.pp_expr_annot)
272
    m.mannot
273

    
274
let pp_machines = pp_print_list ~pp_open_box:pp_open_vbox0 pp_machine
275

    
276
let rec is_const_value v =
277
  match v.value_desc with
278
  | Cst _ ->
279
    true
280
  | Fun (_, args) ->
281
    Basic_library.is_value_internal_fun v && List.for_all is_const_value args
282
  | _ ->
283
    false
284

    
285
(* Returns the declared stateless status and the computed one. *)
286
let get_stateless_status_node n =
287
  ( n.node_dec_stateless,
288
    try Utils.desome n.node_stateless
289
    with _ ->
290
      failwith ("stateless status of machine " ^ n.node_id ^ " not computed") )
291

    
292
let get_stateless_status_top_decl td =
293
  match td.top_decl_desc with
294
  | Node n ->
295
    get_stateless_status_node n
296
  | ImportedNode n ->
297
    n.nodei_stateless, false
298
  | _ ->
299
    true, false
300

    
301
let get_stateless_status m = get_stateless_status_node m.mname
302

    
303
let is_stateless m = m.minstances = [] && m.mmemory = []
304

    
305
(* let is_input m id =
306
 *   List.exists (fun o -> o.var_id = id.var_id) m.mstep.step_inputs *)
307

    
308
let is_output m id =
309
  List.exists (fun o -> o.var_id = id.var_id) m.mstep.step_outputs
310

    
311
let get_instr_spec i = i.instr_spec
312

    
313
let mk_val v t = { value_desc = v; value_type = t; value_annot = None }
314

    
315
let vdecl_to_val vd = mk_val (Var vd) vd.var_type
316

    
317
let vdecls_to_vals = List.map vdecl_to_val
318

    
319
let id_to_tag id =
320
  let typ = (typedef_of_top (Hashtbl.find Corelang.tag_table id)).tydef_id in
321
  mk_val (Cst (Const_tag id)) (Type_predef.type_const typ)
322

    
323
let mk_conditional ?lustre_eq c t e =
324
  mkinstr ?lustre_eq (MBranch (c, [ tag_true, t; tag_false, e ]))
325

    
326
let mk_branch ?lustre_eq c br = mkinstr ?lustre_eq (MBranch (c, br))
327

    
328
let mk_branch' ?lustre_eq v = mk_branch ?lustre_eq (vdecl_to_val v)
329

    
330
let mk_assign ?lustre_eq x v = mkinstr ?lustre_eq (MLocalAssign (x, v))
331

    
332
let arrow_machine =
333
  let state = "_first" in
334
  let var_state = dummy_var_decl state Type_predef.type_bool in
335
  let var_input1 = List.nth Arrow.arrow_desc.node_inputs 0 in
336
  let var_input2 = List.nth Arrow.arrow_desc.node_inputs 1 in
337
  let var_output = List.nth Arrow.arrow_desc.node_outputs 0 in
338
  let cst b = mk_val (Cst (const_of_bool b)) Type_predef.type_bool in
339
  assert (var_input1.var_type = var_input2.var_type);
340
  let t_arg = var_input1.var_type in
341
  (* TODO Xavier: c'est bien la bonne def ? Guillaume: Bof preferable de
342
     reprendre le type des variables non ? *)
343
  {
344
    mname = Arrow.arrow_desc;
345
    mmemory = [ var_state ];
346
    mcalls = [];
347
    minstances = [];
348
    minit = [ mkinstr (MStateAssign (var_state, cst true)) ];
349
    mstatic = [];
350
    mconst = [];
351
    mstep =
352
      {
353
        step_inputs = Arrow.arrow_desc.node_inputs;
354
        step_outputs = Arrow.arrow_desc.node_outputs;
355
        step_locals = [];
356
        step_checks = [];
357
        step_instrs =
358
          [
359
            mk_conditional
360
              (mk_val (Var var_state) Type_predef.type_bool)
361
              (List.map mkinstr
362
                 [
363
                   MStateAssign (var_state, cst false);
364
                   MLocalAssign (var_output, mk_val (Var var_input1) t_arg);
365
                 ])
366
              (List.map mkinstr
367
                 [ MLocalAssign (var_output, mk_val (Var var_input2) t_arg) ]);
368
          ];
369
        step_asserts = [];
370
      };
371
    mspec = { mnode_spec = None; mtransitions = []; mmemory_packs = [] };
372
    mannot = [];
373
    msch = None;
374
  }
375

    
376
let empty_desc =
377
  {
378
    node_id = Arrow.arrow_id;
379
    node_type = Types.bottom;
380
    node_clock = Clocks.bottom;
381
    node_inputs = [];
382
    node_outputs = [];
383
    node_locals = [];
384
    node_gencalls = [];
385
    node_checks = [];
386
    node_asserts = [];
387
    node_stmts = [];
388
    node_dec_stateless = true;
389
    node_stateless = Some true;
390
    node_spec = None;
391
    node_annot = [];
392
    node_iscontract = false;
393
  }
394

    
395
let empty_machine =
396
  {
397
    mname = empty_desc;
398
    mmemory = [];
399
    mcalls = [];
400
    minstances = [];
401
    minit = [];
402
    mstatic = [];
403
    mconst = [];
404
    mstep =
405
      {
406
        step_inputs = [];
407
        step_outputs = [];
408
        step_locals = [];
409
        step_checks = [];
410
        step_instrs = [];
411
        step_asserts = [];
412
      };
413
    mspec = { mnode_spec = None; mtransitions = []; mmemory_packs = [] };
414
    mannot = [];
415
    msch = None;
416
  }
417

    
418
let new_instance =
419
  let cpt = ref (-1) in
420
  fun callee tag ->
421
    let o =
422
      if Stateless.check_node callee then node_name callee
423
      else
424
        Printf.sprintf "ni_%d"
425
          (incr cpt;
426
           !cpt)
427
    in
428
    let o =
429
      if !Options.ansi && is_generic_node callee then
430
        Printf.sprintf "%s_inst_%d" o
431
          (incr cpt;
432
           !cpt)
433
      else o
434
    in
435
    o
436

    
437
let get_machine_opt machines name =
438
  List.fold_left
439
    (fun res m ->
440
      match res with
441
      | Some _ ->
442
        res
443
      | None ->
444
        if m.mname.node_id = name then Some m else None)
445
    None machines
446

    
447
let get_machine machines node_name =
448
  try Utils.desome (get_machine_opt machines node_name)
449
  with Utils.DeSome ->
450
    eprintf "Unable to find machine %s in machines %a@.@?" node_name
451
      (Utils.fprintf_list ~sep:", " (fun fmt m ->
452
           pp_print_string fmt m.mname.node_id))
453
      machines;
454
    assert false
455

    
456
let get_const_assign m id =
457
  try
458
    match
459
      get_instr_desc
460
        (List.find
461
           (fun instr ->
462
             match get_instr_desc instr with
463
             | MLocalAssign (v, _) ->
464
               v == id
465
             | _ ->
466
               false)
467
           m.mconst)
468
    with
469
    | MLocalAssign (_, e) ->
470
      e
471
    | _ ->
472
      assert false
473
  with Not_found -> assert false
474

    
475
let value_of_ident loc m id =
476
  (* is is a state var *)
477
  try
478
    let v = List.find (fun v -> v.var_id = id) m.mmemory in
479
    mk_val (Var v) v.var_type
480
  with Not_found -> (
481
    try
482
      (* id is a node var *)
483
      let v = get_node_var id m.mname in
484
      mk_val (Var v) v.var_type
485
    with Not_found -> (
486
      try
487
        (* id is a constant *)
488
        let c =
489
          Corelang.var_decl_of_const
490
            (const_of_top (Hashtbl.find Corelang.consts_table id))
491
        in
492
        mk_val (Var c) c.var_type
493
      with Not_found ->
494
        (* id is a tag *)
495
        let t = Const_tag id in
496
        mk_val (Cst t) (Typing.type_const loc t)))
497

    
498
(* type of internal fun used in dimension expression *)
499
let type_of_value_appl f args =
500
  if List.mem f Basic_library.arith_funs then (List.hd args).value_type
501
  else Type_predef.type_bool
502

    
503
let rec value_of_dimension m dim =
504
  match dim.Dimension.dim_desc with
505
  | Dimension.Dbool b ->
506
    mk_val
507
      (Cst (Const_tag (if b then tag_true else tag_false)))
508
      Type_predef.type_bool
509
  | Dimension.Dint i ->
510
    mk_val (Cst (Const_int i)) Type_predef.type_int
511
  | Dimension.Dident v ->
512
    value_of_ident dim.Dimension.dim_loc m v
513
  | Dimension.Dappl (f, args) ->
514
    let vargs = List.map (value_of_dimension m) args in
515
    mk_val (Fun (f, vargs)) (type_of_value_appl f vargs)
516
  | Dimension.Dite (i, t, e) -> (
517
    match List.map (value_of_dimension m) [ i; t; e ] with
518
    | [ vi; vt; ve ] ->
519
      mk_val (Fun ("ite", [ vi; vt; ve ])) vt.value_type
520
    | _ ->
521
      assert false)
522
  | Dimension.Dlink dim' ->
523
    value_of_dimension m dim'
524
  | _ ->
525
    assert false
526

    
527
let rec dimension_of_value value =
528
  match value.value_desc with
529
  | Cst (Const_tag t) when t = tag_true ->
530
    Dimension.mkdim_bool Location.dummy_loc true
531
  | Cst (Const_tag t) when t = tag_false ->
532
    Dimension.mkdim_bool Location.dummy_loc false
533
  | Cst (Const_int i) ->
534
    Dimension.mkdim_int Location.dummy_loc i
535
  | Var v ->
536
    Dimension.mkdim_ident Location.dummy_loc v.var_id
537
  | Fun (f, args) ->
538
    Dimension.mkdim_appl Location.dummy_loc f (List.map dimension_of_value args)
539
  | _ ->
540
    assert false
541

    
542
let rec join_branches hl1 hl2 =
543
  match hl1, hl2 with
544
  | [], _ ->
545
    hl2
546
  | _, [] ->
547
    hl1
548
  | (t1, h1) :: q1, (t2, h2) :: q2 ->
549
    if t1 < t2 then (t1, h1) :: join_branches q1 hl2
550
    else if t1 > t2 then (t2, h2) :: join_branches hl1 q2
551
    else (t1, List.fold_right join_guards h1 h2) :: join_branches q1 q2
552

    
553
and join_guards inst1 insts2 =
554
  match get_instr_desc inst1, insts2 with
555
  | ( MBranch (x1, hl1),
556
      ({ instr_desc = MBranch (x2, hl2); _ } as inst2) :: insts2 )
557
    when x1 = x2 ->
558
    mkinstr
559
      ~instr_spec:(get_instr_spec inst1 @ get_instr_spec inst2)
560
      (* TODO on pourrait uniquement concatener les lustres de inst1 et
561
         hd(inst2) *)
562
      (MBranch (x1, join_branches (sort_handlers hl1) (sort_handlers hl2)))
563
    :: insts2
564
  | _ ->
565
    inst1 :: insts2
566

    
567
let join_guards_list insts = List.fold_right join_guards insts []
(33-33/66)