Project

General

Profile

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

    
8
let print_statelocaltag = true
9

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

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

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

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

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

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

    
57
  let pp_predicate m fmt p =
58
    let pp_expr : type a. formatter -> (value_t, a) expression_t -> unit =
59
     fun fmt e -> pp_expr m fmt e
60
    in
61
    match p with
62
    | Transition (f, inst, i, vars, _r, _mems, _insts) ->
63
      fprintf
64
        fmt
65
        "Transition_%a<%a>%a%a"
66
        pp_print_string
67
        f
68
        (pp_print_option
69
           ~none:(fun fmt () -> pp_print_string fmt "SELF")
70
           pp_print_string)
71
        inst
72
        (pp_print_option pp_print_int)
73
        i
74
        (pp_print_parenthesized pp_expr)
75
        vars
76
    | Reset (f, inst, r) ->
77
      fprintf
78
        fmt
79
        "Reset_%a<%a> on %a"
80
        pp_print_string
81
        f
82
        pp_print_string
83
        inst
84
        (pp_val m)
85
        r
86
    | MemoryPack (f, inst, i) ->
87
      fprintf
88
        fmt
89
        "MemoryPack_%a<%a>%a"
90
        pp_print_string
91
        f
92
        (pp_print_option
93
           ~none:(fun fmt () -> pp_print_string fmt "SELF")
94
           pp_print_string)
95
        inst
96
        (pp_print_option pp_print_int)
97
        i
98
    | ResetCleared f ->
99
      fprintf fmt "ResetCleared_%a" pp_print_string f
100
    | Initialization ->
101
      ()
102

    
103
  let pp_spec m =
104
    let pp_expr : type a. formatter -> (value_t, a) expression_t -> unit =
105
     fun fmt e -> pp_expr m fmt e
106
    in
107
    let rec pp_spec fmt f =
108
      match f with
109
      | True ->
110
        pp_print_string fmt "true"
111
      | False ->
112
        pp_print_string fmt "false"
113
      | Equal (a, b) ->
114
        fprintf fmt "%a == %a" pp_expr a pp_expr b
115
      | And fs ->
116
        pp_print_list
117
          ~pp_sep:(fun fmt () -> fprintf fmt "@ ∧ ")
118
          (fun fmt spec -> fprintf fmt "@[%a@]" pp_spec spec)
119
          fmt
120
          fs
121
      | Or fs ->
122
        pp_print_list
123
          ~pp_sep:(fun fmt () -> fprintf fmt "@ ∨ ")
124
          (fun fmt spec -> fprintf fmt "@[%a@]" pp_spec spec)
125
          fmt
126
          fs
127
      | Imply (a, b) ->
128
        fprintf fmt "%a@ -> %a" pp_spec a pp_spec b
129
      | Exists (xs, a) ->
130
        fprintf
131
          fmt
132
          "@[<hv 2>∃ @[<h>%a,@]@ %a@]"
133
          (pp_comma_list Printers.pp_var)
134
          xs
135
          pp_spec
136
          a
137
      | Forall (xs, a) ->
138
        fprintf
139
          fmt
140
          "@[<hv 2>∀ @[<h>%a,@]@ %a@]"
141
          (pp_comma_list Printers.pp_var)
142
          xs
143
          pp_spec
144
          a
145
      | Ternary (e, a, b) ->
146
        fprintf
147
          fmt
148
          "If %a Then (@[<hov>%a@]) Else (@[<hov>%a@])"
149
          pp_expr
150
          e
151
          pp_spec
152
          a
153
          pp_spec
154
          b
155
      | Predicate p ->
156
        pp_predicate m fmt p
157
      | StateVarPack r ->
158
        fprintf fmt "StateVarPack<%a>" pp_reg r
159
      | ExistsMem (_f, a, b) ->
160
        fprintf fmt "@[<hv 2>∃ MEM,@ %a@]" pp_spec (And [ a; b ])
161
      | Value v ->
162
        pp_val m fmt v
163

    
164
    in
165
    pp_spec
166
end
167

    
168
let pp_spec m =
169
  match !Options.spec with
170
  | Options.SpecNo ->
171
    pp_print_nothing
172
  | _ ->
173
    pp_print_list
174
      ~pp_open_box:pp_open_vbox0
175
      ~pp_prologue:pp_print_cut
176
      (fun fmt -> fprintf fmt "@[<h>--%@ %a@]" (PrintSpec.pp_spec m))
177

    
178
let rec pp_instr m fmt i =
179
  let pp_val = pp_val m in
180
  let pp_branch = pp_branch m in
181
  (match i.instr_desc with
182
  | MLocalAssign (i, v) ->
183
    fprintf fmt "%s := %a" i.var_id pp_val v
184
  | MStateAssign (i, v) ->
185
    fprintf fmt "{%s} := %a" i.var_id pp_val v
186
  | MResetAssign b ->
187
    fprintf fmt "RESET := %a" pp_print_bool b
188
  | MSetReset i ->
189
    fprintf fmt "set_reset %s" i
190
  | MClearReset ->
191
    fprintf fmt "clear_reset %s" m.mname.node_id
192
  | MNoReset i ->
193
    fprintf fmt "noreset %s" i
194
  | MStep (il, i, vl) ->
195
    fprintf
196
      fmt
197
      "%a := %s%a"
198
      (pp_comma_list pp_vdecl)
199
      il
200
      i
201
      (pp_print_parenthesized pp_val)
202
      vl
203
  | MBranch (g, hl) ->
204
    fprintf
205
      fmt
206
      "@[<v 2>case(%a) {@,%a@]@,}"
207
      pp_val
208
      g
209
      (pp_print_list ~pp_open_box:pp_open_vbox0 pp_branch)
210
      hl
211
  | MComment s ->
212
    pp_print_string fmt s
213
  | MSpec s ->
214
    pp_print_string fmt ("@" ^ s));
215
  (* Annotation *)
216
  (* let _ = *)
217
  (* match i.lustre_expr with None -> () | Some e -> fprintf fmt " -- original
218
     expr: %a" Printers.pp_expr e *)
219
  (* in *)
220
  (match i.lustre_eq with
221
  | None ->
222
    ()
223
  | Some eq ->
224
    fprintf fmt " @[<h>-- original eq: %a@]" Printers.pp_node_eq eq);
225
  pp_spec m fmt i.instr_spec
226

    
227
and pp_branch m fmt (t, h) =
228
  fprintf
229
    fmt
230
    "@[<v 2>%s:@,%a@]"
231
    t
232
    (pp_print_list ~pp_open_box:pp_open_vbox0 (pp_instr m))
233
    h
234

    
235
let pp_instrs m = pp_print_list ~pp_open_box:pp_open_vbox0 (pp_instr m)
236

    
237
(* merge log: get_node_def was in c0f8 *)
238
(* Returns the node/machine associated to id in m calls *)
239
let get_node_def id m =
240
  try
241
    let decl, _ = List.assoc id m.mcalls in
242
    Corelang.node_of_top decl
243
  with Not_found ->
244
    (* eprintf "Unable to find node %s in list [%a]@.@?" *)
245
    (*   id *)
246
    (* (Utils.fprintf_list ~sep:", " (fun fmt (n,_) -> fprintf fmt "%s" n))
247
       m.mcalls *)
248
    (* ; *)
249
    raise Not_found
250

    
251
(* merge log: machine_vars was in 44686 *)
252
let machine_vars m =
253
  m.mstep.step_inputs @ m.mstep.step_locals @ m.mstep.step_outputs @ m.mmemory
254

    
255
let pp_step m fmt s =
256
  fprintf
257
    fmt
258
    "@[<v>inputs : %a@ outputs: %a@ locals : %a@ checks : %a@ instrs : @[%a@]@ \
259
     asserts : @[%a@]@]@ "
260
    (pp_comma_list Printers.pp_var)
261
    s.step_inputs
262
    (pp_comma_list Printers.pp_var)
263
    s.step_outputs
264
    (pp_comma_list Printers.pp_var)
265
    s.step_locals
266
    (pp_comma_list (fun fmt (_, c) -> pp_val m fmt c))
267
    s.step_checks
268
    (pp_instrs m)
269
    s.step_instrs
270
    (pp_comma_list (pp_val m))
271
    s.step_asserts
272

    
273
let pp_static_call fmt (node, args) =
274
  fprintf fmt "%s<%a>" (node_name node) (pp_comma_list Dimension.pp) args
275

    
276
let pp_instance fmt (o1, o2) = fprintf fmt "(%s, %a)" o1 pp_static_call o2
277

    
278
let pp_memory_pack m fmt mp =
279
  fprintf
280
    fmt
281
    "@[<v 2>MemoryPack_%a<SELF>%a =@ %a@]"
282
    pp_print_string
283
    mp.mpname.node_id
284
    (pp_print_option pp_print_int)
285
    mp.mpindex
286
    (PrintSpec.pp_spec m)
287
    mp.mpformula
288

    
289
let pp_memory_packs m fmt =
290
  match !Options.spec with
291
  | Options.SpecNo ->
292
    pp_print_nothing fmt
293
  | _ ->
294
    fprintf fmt "@[<v 2>memory_packs:@ %a@]" (pp_print_list (pp_memory_pack m))
295

    
296
let pp_transition m fmt t =
297
  fprintf
298
    fmt
299
    "@[<v 2>Transition_%a<SELF>%a%a =@ %a@]"
300
    pp_print_string
301
    t.tname.node_id
302
    (pp_print_option pp_print_int)
303
    t.tindex
304
    (pp_print_parenthesized pp_vdecl)
305
    t.tvars
306
    (PrintSpec.pp_spec m)
307
    t.tformula
308

    
309
let pp_transitions m fmt =
310
  match !Options.spec with
311
  | Options.SpecNo ->
312
    pp_print_nothing fmt
313
  | _ ->
314
    fprintf fmt "@[<v 2>transitions:@ %a@]" (pp_print_list (pp_transition m))
315

    
316
let pp_mspec m fmt c =
317
  fprintf fmt "@[<v>contract: G (H (%a) => %a);]"
318
    (PrintSpec.pp_spec m) c.mc_pre
319
    (PrintSpec.pp_spec m) c.mc_post
320

    
321
let pp_machine fmt m =
322
  fprintf
323
    fmt
324
    "@[<v 2>machine %s@ mem      : %a@ instances: %a@ init     : %a@ const    \
325
     : %a@ step     :@   @[<v 2>%a@]@ spec     : @[<v>%t@ %a@ @ %a@]@ annot    \
326
     : @[%a@]@]@ "
327
    m.mname.node_id
328
    (pp_comma_list Printers.pp_var)
329
    m.mmemory
330
    (pp_comma_list pp_instance)
331
    m.minstances
332
    (pp_instrs m)
333
    m.minit
334
    (pp_instrs m)
335
    m.mconst
336
    (pp_step m)
337
    m.mstep
338
    (fun fmt ->
339
      match m.mspec.mnode_spec with
340
      | None ->
341
        ()
342
      | Some (NodeSpec id) ->
343
        fprintf fmt "cocospec: %s" id
344
      | Some (Contract spec) ->
345
        pp_mspec m fmt spec)
346
    (pp_memory_packs m)
347
    m.mspec.mmemory_packs
348
    (pp_transitions m)
349
    m.mspec.mtransitions
350
    (pp_print_list Printers.pp_expr_annot)
351
    m.mannot
352

    
353
let pp_machines = pp_print_list ~pp_open_box:pp_open_vbox0 pp_machine
354

    
355
let rec is_const_value v =
356
  match v.value_desc with
357
  | Cst _ ->
358
    true
359
  | Fun (_, args) ->
360
    Basic_library.is_value_internal_fun v && List.for_all is_const_value args
361
  | _ ->
362
    false
363

    
364
(* Returns the declared stateless status and the computed one. *)
365
let get_stateless_status_node n =
366
  ( n.node_dec_stateless,
367
    try Utils.desome n.node_stateless
368
    with _ ->
369
      failwith ("stateless status of machine " ^ n.node_id ^ " not computed") )
370

    
371
let get_stateless_status_top_decl td =
372
  match td.top_decl_desc with
373
  | Node n ->
374
    get_stateless_status_node n
375
  | ImportedNode n ->
376
    n.nodei_stateless, false
377
  | _ ->
378
    true, false
379

    
380
let get_stateless_status m = get_stateless_status_node m.mname
381

    
382
let is_stateless m = m.minstances = [] && m.mmemory = []
383

    
384
(* let is_input m id =
385
 *   List.exists (fun o -> o.var_id = id.var_id) m.mstep.step_inputs *)
386

    
387
let is_output m id =
388
  List.exists (fun o -> o.var_id = id.var_id) m.mstep.step_outputs
389

    
390
let get_instr_spec i = i.instr_spec
391

    
392
let mk_val v t = { value_desc = v; value_type = t; value_annot = None }
393

    
394
let vdecl_to_val vd = mk_val (Var vd) vd.var_type
395

    
396
let vdecls_to_vals = List.map vdecl_to_val
397

    
398
let id_to_tag id =
399
  let typ = (typedef_of_top (Hashtbl.find Corelang.tag_table id)).tydef_id in
400
  mk_val (Cst (Const_tag id)) (Type_predef.type_const typ)
401

    
402
let mk_conditional ?lustre_eq c t e =
403
  mkinstr ?lustre_eq (MBranch (c, [ tag_true, t; tag_false, e ]))
404

    
405
let mk_branch ?lustre_eq c br = mkinstr ?lustre_eq (MBranch (c, br))
406

    
407
let mk_branch' ?lustre_eq v = mk_branch ?lustre_eq (vdecl_to_val v)
408

    
409
let mk_assign ?lustre_eq x v = mkinstr ?lustre_eq (MLocalAssign (x, v))
410

    
411
let arrow_machine =
412
  let state = "_first" in
413
  let var_state = dummy_var_decl state Type_predef.type_bool in
414
  let var_input1 = List.nth Arrow.arrow_desc.node_inputs 0 in
415
  let var_input2 = List.nth Arrow.arrow_desc.node_inputs 1 in
416
  let var_output = List.nth Arrow.arrow_desc.node_outputs 0 in
417
  let cst b = mk_val (Cst (const_of_bool b)) Type_predef.type_bool in
418
  assert (var_input1.var_type = var_input2.var_type);
419
  let t_arg = var_input1.var_type in
420
  (* TODO Xavier: c'est bien la bonne def ? Guillaume: Bof preferable de
421
     reprendre le type des variables non ? *)
422
  {
423
    mname = Arrow.arrow_desc;
424
    mmemory = [ var_state ];
425
    mcalls = [];
426
    minstances = [];
427
    minit = [ mkinstr (MStateAssign (var_state, cst true)) ];
428
    mstatic = [];
429
    mconst = [];
430
    mstep =
431
      {
432
        step_inputs = Arrow.arrow_desc.node_inputs;
433
        step_outputs = Arrow.arrow_desc.node_outputs;
434
        step_locals = [];
435
        step_checks = [];
436
        step_instrs =
437
          [
438
            mk_conditional
439
              (mk_val (Var var_state) Type_predef.type_bool)
440
              (List.map
441
                 mkinstr
442
                 [
443
                   MStateAssign (var_state, cst false);
444
                   MLocalAssign (var_output, mk_val (Var var_input1) t_arg);
445
                 ])
446
              (List.map
447
                 mkinstr
448
                 [ MLocalAssign (var_output, mk_val (Var var_input2) t_arg) ]);
449
          ];
450
        step_asserts = [];
451
      };
452
    mspec = { mnode_spec = None; mtransitions = []; mmemory_packs = [] };
453
    mannot = [];
454
    msch = None;
455
    mis_contract = false
456
  }
457

    
458
let empty_desc =
459
  {
460
    node_id = Arrow.arrow_id;
461
    node_type = Types.bottom;
462
    node_clock = Clocks.bottom;
463
    node_inputs = [];
464
    node_outputs = [];
465
    node_locals = [];
466
    node_gencalls = [];
467
    node_checks = [];
468
    node_asserts = [];
469
    node_stmts = [];
470
    node_dec_stateless = true;
471
    node_stateless = Some true;
472
    node_spec = None;
473
    node_annot = [];
474
    node_iscontract = false;
475
  }
476

    
477
let empty_machine =
478
  {
479
    mname = empty_desc;
480
    mmemory = [];
481
    mcalls = [];
482
    minstances = [];
483
    minit = [];
484
    mstatic = [];
485
    mconst = [];
486
    mstep =
487
      {
488
        step_inputs = [];
489
        step_outputs = [];
490
        step_locals = [];
491
        step_checks = [];
492
        step_instrs = [];
493
        step_asserts = [];
494
      };
495
    mspec = { mnode_spec = None; mtransitions = []; mmemory_packs = [] };
496
    mannot = [];
497
    msch = None;
498
    mis_contract = false
499
  }
500

    
501
let new_instance =
502
  let cpt = ref (-1) in
503
  fun callee tag ->
504
    let o =
505
      if Stateless.check_node callee then node_name callee
506
      else
507
        Printf.sprintf
508
          "ni_%d"
509
          (incr cpt;
510
           !cpt)
511
    in
512
    let o =
513
      if !Options.ansi && is_generic_node callee then
514
        Printf.sprintf
515
          "%s_inst_%d"
516
          o
517
          (incr cpt;
518
           !cpt)
519
      else o
520
    in
521
    o
522

    
523
let get_machine_opt machines name =
524
  List.fold_left
525
    (fun res m ->
526
      match res with
527
      | Some _ ->
528
        res
529
      | None ->
530
        if m.mname.node_id = name then Some m else None)
531
    None
532
    machines
533

    
534
let get_machine machines node_name =
535
  try desome (get_machine_opt machines node_name)
536
  with DeSome ->
537
    eprintf
538
      "Unable to find machine %s in machines %a@.@?"
539
      node_name
540
      (pp_comma_list (fun fmt m -> pp_print_string fmt m.mname.node_id))
541
      machines;
542
    assert false
543

    
544
let get_const_assign m id =
545
  try
546
    match
547
      get_instr_desc
548
        (List.find
549
           (fun instr ->
550
             match get_instr_desc instr with
551
             | MLocalAssign (v, _) ->
552
               v == id
553
             | _ ->
554
               false)
555
           m.mconst)
556
    with
557
    | MLocalAssign (_, e) ->
558
      e
559
    | _ ->
560
      assert false
561
  with Not_found -> assert false
562

    
563
let value_of_ident loc m id =
564
  (* is is a state var *)
565
  try
566
    let v = List.find (fun v -> v.var_id = id) m.mmemory in
567
    mk_val (Var v) v.var_type
568
  with Not_found -> (
569
    try
570
      (* id is a node var *)
571
      let v = get_node_var id m.mname in
572
      mk_val (Var v) v.var_type
573
    with Not_found -> (
574
      try
575
        (* id is a constant *)
576
        let c =
577
          Corelang.var_decl_of_const
578
            (const_of_top (Hashtbl.find Corelang.consts_table id))
579
        in
580
        mk_val (Var c) c.var_type
581
      with Not_found ->
582
        (* id is a tag *)
583
        let t = Const_tag id in
584
        mk_val (Cst t) (Typing.type_const loc t)))
585

    
586
(* type of internal fun used in dimension expression *)
587
let type_of_value_appl f args =
588
  if List.mem f Basic_library.arith_funs then (List.hd args).value_type
589
  else Type_predef.type_bool
590

    
591
let rec value_of_dimension m dim =
592
  match dim.Dimension.dim_desc with
593
  | Dimension.Dbool b ->
594
    mk_val
595
      (Cst (Const_tag (if b then tag_true else tag_false)))
596
      Type_predef.type_bool
597
  | Dimension.Dint i ->
598
    mk_val (Cst (Const_int i)) Type_predef.type_int
599
  | Dimension.Dident v ->
600
    value_of_ident dim.Dimension.dim_loc m v
601
  | Dimension.Dappl (f, args) ->
602
    let vargs = List.map (value_of_dimension m) args in
603
    mk_val (Fun (f, vargs)) (type_of_value_appl f vargs)
604
  | Dimension.Dite (i, t, e) -> (
605
    match List.map (value_of_dimension m) [ i; t; e ] with
606
    | [ vi; vt; ve ] ->
607
      mk_val (Fun ("ite", [ vi; vt; ve ])) vt.value_type
608
    | _ ->
609
      assert false)
610
  | Dimension.Dlink dim' ->
611
    value_of_dimension m dim'
612
  | _ ->
613
    assert false
614

    
615
let rec dimension_of_value value =
616
  match value.value_desc with
617
  | Cst (Const_tag t) when t = tag_true ->
618
    Dimension.mkdim_bool Location.dummy true
619
  | Cst (Const_tag t) when t = tag_false ->
620
    Dimension.mkdim_bool Location.dummy false
621
  | Cst (Const_int i) ->
622
    Dimension.mkdim_int Location.dummy i
623
  | Var v ->
624
    Dimension.mkdim_ident Location.dummy v.var_id
625
  | Fun (f, args) ->
626
    Dimension.mkdim_appl Location.dummy f (List.map dimension_of_value args)
627
  | _ ->
628
    assert false
629

    
630
let rec join_branches hl1 hl2 =
631
  match hl1, hl2 with
632
  | [], _ ->
633
    hl2
634
  | _, [] ->
635
    hl1
636
  | (t1, h1) :: q1, (t2, h2) :: q2 ->
637
    if t1 < t2 then (t1, h1) :: join_branches q1 hl2
638
    else if t1 > t2 then (t2, h2) :: join_branches hl1 q2
639
    else (t1, List.fold_right join_guards h1 h2) :: join_branches q1 q2
640

    
641
and join_guards inst1 insts2 =
642
  match get_instr_desc inst1, insts2 with
643
  | ( MBranch (x1, hl1),
644
      ({ instr_desc = MBranch (x2, hl2); _ } as inst2) :: insts2 )
645
    when x1 = x2 ->
646
    mkinstr
647
      ~instr_spec:(get_instr_spec inst1 @ get_instr_spec inst2)
648
      (* TODO on pourrait uniquement concatener les lustres de inst1 et
649
         hd(inst2) *)
650
      (MBranch (x1, join_branches (sort_handlers hl1) (sort_handlers hl2)))
651
    :: insts2
652
  | _ ->
653
    inst1 :: insts2
654

    
655
let join_guards_list insts = List.fold_right join_guards insts []
(48-48/99)