Project

General

Profile

Download (16.7 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) ->
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
325
    (* (Ternary (Val c,
326
     *           And (List.map get_instr_spec t),
327
     *           And (List.map get_instr_spec e))) *)
328
    (MBranch (c, [ tag_true, t; tag_false, e ]))
329

    
330
let mk_branch ?lustre_eq c br =
331
  mkinstr ?lustre_eq
332
    (* (And (List.map (fun (l, instrs) ->
333
     *      Imply (Equal (Val c, Tag l), And (List.map get_instr_spec instrs)))
334
     *      br)) *)
335
    (MBranch (c, br))
336

    
337
let mk_branch' ?lustre_eq v = mk_branch ?lustre_eq (vdecl_to_val v)
338

    
339
let mk_assign ?lustre_eq x v =
340
  mkinstr ?lustre_eq (* (Equal (Var x, Val v)) *) (MLocalAssign (x, v))
341

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

    
389
let empty_desc =
390
  {
391
    node_id = Arrow.arrow_id;
392
    node_type = Types.bottom;
393
    node_clock = Clocks.bottom;
394
    node_inputs = [];
395
    node_outputs = [];
396
    node_locals = [];
397
    node_gencalls = [];
398
    node_checks = [];
399
    node_asserts = [];
400
    node_stmts = [];
401
    node_dec_stateless = true;
402
    node_stateless = Some true;
403
    node_spec = None;
404
    node_annot = [];
405
    node_iscontract = false;
406
  }
407

    
408
let empty_machine =
409
  {
410
    mname = empty_desc;
411
    mmemory = [];
412
    mcalls = [];
413
    minstances = [];
414
    minit = [];
415
    mstatic = [];
416
    mconst = [];
417
    mstep =
418
      {
419
        step_inputs = [];
420
        step_outputs = [];
421
        step_locals = [];
422
        step_checks = [];
423
        step_instrs = [];
424
        step_asserts = [];
425
      };
426
    mspec = { mnode_spec = None; mtransitions = []; mmemory_packs = [] };
427
    mannot = [];
428
    msch = None;
429
  }
430

    
431
let new_instance =
432
  let cpt = ref (-1) in
433
  fun callee tag ->
434
    let o =
435
      if Stateless.check_node callee then node_name callee
436
      else
437
        Printf.sprintf "ni_%d"
438
          (incr cpt;
439
           !cpt)
440
    in
441
    let o =
442
      if !Options.ansi && is_generic_node callee then
443
        Printf.sprintf "%s_inst_%d" o
444
          (incr cpt;
445
           !cpt)
446
      else o
447
    in
448
    o
449

    
450
let get_machine_opt machines name =
451
  List.fold_left
452
    (fun res m ->
453
      match res with
454
      | Some _ ->
455
        res
456
      | None ->
457
        if m.mname.node_id = name then Some m else None)
458
    None machines
459

    
460
let get_machine machines node_name =
461
  try Utils.desome (get_machine_opt machines node_name)
462
  with Utils.DeSome ->
463
    eprintf "Unable to find machine %s in machines %a@.@?" node_name
464
      (Utils.fprintf_list ~sep:", " (fun fmt m ->
465
           pp_print_string fmt m.mname.node_id))
466
      machines;
467
    assert false
468

    
469
let get_const_assign m id =
470
  try
471
    match
472
      get_instr_desc
473
        (List.find
474
           (fun instr ->
475
             match get_instr_desc instr with
476
             | MLocalAssign (v, _) ->
477
               v == id
478
             | _ ->
479
               false)
480
           m.mconst)
481
    with
482
    | MLocalAssign (_, e) ->
483
      e
484
    | _ ->
485
      assert false
486
  with Not_found -> assert false
487

    
488
let value_of_ident loc m id =
489
  (* is is a state var *)
490
  try
491
    let v = List.find (fun v -> v.var_id = id) m.mmemory in
492
    mk_val (Var v) v.var_type
493
  with Not_found -> (
494
    try
495
      (* id is a node var *)
496
      let v = get_node_var id m.mname in
497
      mk_val (Var v) v.var_type
498
    with Not_found -> (
499
      try
500
        (* id is a constant *)
501
        let c =
502
          Corelang.var_decl_of_const
503
            (const_of_top (Hashtbl.find Corelang.consts_table id))
504
        in
505
        mk_val (Var c) c.var_type
506
      with Not_found ->
507
        (* id is a tag *)
508
        let t = Const_tag id in
509
        mk_val (Cst t) (Typing.type_const loc t)))
510

    
511
(* type of internal fun used in dimension expression *)
512
let type_of_value_appl f args =
513
  if List.mem f Basic_library.arith_funs then (List.hd args).value_type
514
  else Type_predef.type_bool
515

    
516
let rec value_of_dimension m dim =
517
  match dim.Dimension.dim_desc with
518
  | Dimension.Dbool b ->
519
    mk_val
520
      (Cst (Const_tag (if b then tag_true else tag_false)))
521
      Type_predef.type_bool
522
  | Dimension.Dint i ->
523
    mk_val (Cst (Const_int i)) Type_predef.type_int
524
  | Dimension.Dident v ->
525
    value_of_ident dim.Dimension.dim_loc m v
526
  | Dimension.Dappl (f, args) ->
527
    let vargs = List.map (value_of_dimension m) args in
528
    mk_val (Fun (f, vargs)) (type_of_value_appl f vargs)
529
  | Dimension.Dite (i, t, e) -> (
530
    match List.map (value_of_dimension m) [ i; t; e ] with
531
    | [ vi; vt; ve ] ->
532
      mk_val (Fun ("ite", [ vi; vt; ve ])) vt.value_type
533
    | _ ->
534
      assert false)
535
  | Dimension.Dlink dim' ->
536
    value_of_dimension m dim'
537
  | _ ->
538
    assert false
539

    
540
let rec dimension_of_value value =
541
  match value.value_desc with
542
  | Cst (Const_tag t) when t = tag_true ->
543
    Dimension.mkdim_bool Location.dummy_loc true
544
  | Cst (Const_tag t) when t = tag_false ->
545
    Dimension.mkdim_bool Location.dummy_loc false
546
  | Cst (Const_int i) ->
547
    Dimension.mkdim_int Location.dummy_loc i
548
  | Var v ->
549
    Dimension.mkdim_ident Location.dummy_loc v.var_id
550
  | Fun (f, args) ->
551
    Dimension.mkdim_appl Location.dummy_loc f (List.map dimension_of_value args)
552
  | _ ->
553
    assert false
554

    
555
let rec join_branches hl1 hl2 =
556
  match hl1, hl2 with
557
  | [], _ ->
558
    hl2
559
  | _, [] ->
560
    hl1
561
  | (t1, h1) :: q1, (t2, h2) :: q2 ->
562
    if t1 < t2 then (t1, h1) :: join_branches q1 hl2
563
    else if t1 > t2 then (t2, h2) :: join_branches hl1 q2
564
    else (t1, List.fold_right join_guards h1 h2) :: join_branches q1 q2
565

    
566
and join_guards inst1 insts2 =
567
  match get_instr_desc inst1, insts2 with
568
  | ( MBranch (x1, hl1),
569
      ({ instr_desc = MBranch (x2, hl2); _ } as inst2) :: insts2 )
570
    when x1 = x2 ->
571
    mkinstr
572
      ~instr_spec:(get_instr_spec inst1 @ get_instr_spec inst2)
573
      (* TODO on pourrait uniquement concatener les lustres de inst1 et
574
         hd(inst2) *)
575
      (MBranch (x1, join_branches (sort_handlers hl1) (sort_handlers hl2)))
576
    :: insts2
577
  | _ ->
578
    inst1 :: insts2
579

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