Project

General

Profile

Download (16.9 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 m fmt = function
46
    | Val v ->
47
      pp_val m fmt v
48
    | Tag (t, _) ->
49
      pp_print_string fmt t
50
    | Var v ->
51
      pp_vdecl fmt v
52
    | Memory r ->
53
      pp_reg fmt r
54

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

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

    
161
    pp_spec
162
end
163

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

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

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

    
231
let pp_instrs m = pp_print_list ~pp_open_box:pp_open_vbox0 (pp_instr m)
232

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

    
247
(* merge log: machine_vars was in 44686 *)
248
let machine_vars m =
249
  m.mstep.step_inputs @ m.mstep.step_locals @ m.mstep.step_outputs @ m.mmemory
250

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

    
269
let pp_static_call fmt (node, args) =
270
  fprintf fmt "%s<%a>" (node_name node) (pp_comma_list Dimension.pp) args
271

    
272
let pp_instance fmt (o1, o2) = fprintf fmt "(%s, %a)" o1 pp_static_call o2
273

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

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

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

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

    
312
let pp_mspec m fmt c =
313
  fprintf
314
    fmt
315
    "@[<v>contract: G (H (%a) => %a);]"
316
    (PrintSpec.pp_spec m)
317
    c.mc_pre
318
    (PrintSpec.pp_spec m)
319
    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)