Project

General

Profile

Download (17.1 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
      | GEqual (a, b) ->
116
        fprintf fmt "%a >= %a" pp_expr a pp_expr b
117
      | And 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
      | Or fs ->
124
        pp_print_list
125
          ~pp_sep:(fun fmt () -> fprintf fmt "@ ∨ ")
126
          (fun fmt spec -> fprintf fmt "@[%a@]" pp_spec spec)
127
          fmt
128
          fs
129
      | Imply (a, b) ->
130
        fprintf fmt "%a@ -> %a" pp_spec a pp_spec b
131
      | Exists (xs, a) ->
132
        fprintf
133
          fmt
134
          "@[<hv 2>∃ @[<h>%a,@]@ %a@]"
135
          (pp_comma_list Printers.pp_var)
136
          xs
137
          pp_spec
138
          a
139
      | Forall (xs, a) ->
140
        fprintf
141
          fmt
142
          "@[<hv 2>∀ @[<h>%a,@]@ %a@]"
143
          (pp_comma_list Printers.pp_var)
144
          xs
145
          pp_spec
146
          a
147
      | Ternary (e, a, b) ->
148
        fprintf
149
          fmt
150
          "If %a Then (@[<hov>%a@]) Else (@[<hov>%a@])"
151
          pp_expr
152
          e
153
          pp_spec
154
          a
155
          pp_spec
156
          b
157
      | Predicate p ->
158
        pp_predicate m fmt p
159
      | StateVarPack r ->
160
        fprintf fmt "StateVarPack<%a>" pp_reg r
161
      | ExistsMem (_f, a, b) ->
162
        fprintf fmt "@[<hv 2>∃ MEM,@ %a@]" pp_spec (And [ a; b ])
163
      | Value v ->
164
        pp_val m fmt v
165
    in
166

    
167
    pp_spec
168
end
169

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

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

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

    
237
let pp_instrs m = pp_print_list ~pp_open_box:pp_open_vbox0 (pp_instr m)
238

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

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

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

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

    
278
let pp_instance fmt (o1, o2) = fprintf fmt "(%s, %a)" o1 pp_static_call o2
279

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

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

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

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

    
318
let pp_mspec m fmt c =
319
  fprintf
320
    fmt
321
    "@[<v>contract: G (H (%a) => %a);]"
322
    (PrintSpec.pp_spec m)
323
    c.mc_pre
324
    (PrintSpec.pp_spec m)
325
    c.mc_post
326

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

    
359
let pp_machines = pp_print_list ~pp_open_box:pp_open_vbox0 pp_machine
360

    
361
let rec is_const_value v =
362
  match v.value_desc with
363
  | Cst _ ->
364
    true
365
  | Fun (_, args) ->
366
    Basic_library.is_value_internal_fun v && List.for_all is_const_value args
367
  | _ ->
368
    false
369

    
370
(* Returns the declared stateless status and the computed one. *)
371
let get_stateless_status_node n =
372
  ( n.node_dec_stateless,
373
    try Utils.desome n.node_stateless
374
    with _ ->
375
      failwith ("stateless status of machine " ^ n.node_id ^ " not computed") )
376

    
377
let get_stateless_status_top_decl td =
378
  match td.top_decl_desc with
379
  | Node n ->
380
    get_stateless_status_node n
381
  | ImportedNode n ->
382
    n.nodei_stateless, false
383
  | _ ->
384
    true, false
385

    
386
let get_stateless_status m = get_stateless_status_node m.mname
387

    
388
let is_stateless m = m.minstances = [] && m.mmemory = []
389

    
390
(* let is_input m id =
391
 *   List.exists (fun o -> o.var_id = id.var_id) m.mstep.step_inputs *)
392

    
393
let is_output m id =
394
  List.exists (fun o -> o.var_id = id.var_id) m.mstep.step_outputs
395

    
396
let get_instr_spec i = i.instr_spec
397

    
398
let mk_val v t = { value_desc = v; value_type = t; value_annot = None }
399

    
400
let vdecl_to_val vd = mk_val (Var vd) vd.var_type
401

    
402
let vdecls_to_vals = List.map vdecl_to_val
403

    
404
let id_to_tag id =
405
  let typ = (typedef_of_top (Hashtbl.find Corelang.tag_table id)).tydef_id in
406
  mk_val (Cst (Const_tag id)) (Type_predef.type_const typ)
407

    
408
let mk_conditional ?lustre_eq c t e =
409
  mkinstr ?lustre_eq (MBranch (c, [ tag_true, t; tag_false, e ]))
410

    
411
let mk_branch ?lustre_eq c br = mkinstr ?lustre_eq (MBranch (c, br))
412

    
413
let mk_branch' ?lustre_eq v = mk_branch ?lustre_eq (vdecl_to_val v)
414

    
415
let mk_assign ?lustre_eq x v = mkinstr ?lustre_eq (MLocalAssign (x, v))
416

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

    
464
let empty_desc =
465
  {
466
    node_id = Arrow.arrow_id;
467
    node_type = Types.bottom;
468
    node_clock = Clocks.bottom;
469
    node_inputs = [];
470
    node_outputs = [];
471
    node_locals = [];
472
    node_gencalls = [];
473
    node_checks = [];
474
    node_asserts = [];
475
    node_stmts = [];
476
    node_dec_stateless = true;
477
    node_stateless = Some true;
478
    node_spec = None;
479
    node_annot = [];
480
    node_iscontract = false;
481
  }
482

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

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

    
529
let get_machine_opt machines name =
530
  List.fold_left
531
    (fun res m ->
532
      match res with
533
      | Some _ ->
534
        res
535
      | None ->
536
        if m.mname.node_id = name then Some m else None)
537
    None
538
    machines
539

    
540
let get_machine machines node_name =
541
  try desome (get_machine_opt machines node_name)
542
  with DeSome ->
543
    eprintf
544
      "Unable to find machine %s in machines %a@.@?"
545
      node_name
546
      (pp_comma_list (fun fmt m -> pp_print_string fmt m.mname.node_id))
547
      machines;
548
    assert false
549

    
550
let get_const_assign m id =
551
  try
552
    match
553
      get_instr_desc
554
        (List.find
555
           (fun instr ->
556
             match get_instr_desc instr with
557
             | MLocalAssign (v, _) ->
558
               v == id
559
             | _ ->
560
               false)
561
           m.mconst)
562
    with
563
    | MLocalAssign (_, e) ->
564
      e
565
    | _ ->
566
      assert false
567
  with Not_found -> assert false
568

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

    
592
(* type of internal fun used in dimension expression *)
593
let type_of_value_appl f args =
594
  if List.mem f Basic_library.arith_funs then (List.hd args).value_type
595
  else Type_predef.type_bool
596

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

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

    
636
let rec join_branches hl1 hl2 =
637
  match hl1, hl2 with
638
  | [], _ ->
639
    hl2
640
  | _, [] ->
641
    hl1
642
  | (t1, h1) :: q1, (t2, h2) :: q2 ->
643
    if t1 < t2 then (t1, h1) :: join_branches q1 hl2
644
    else if t1 > t2 then (t2, h2) :: join_branches hl1 q2
645
    else (t1, List.fold_right join_guards h1 h2) :: join_branches q1 q2
646

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

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