Project

General

Profile

Download (16.3 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, vars, _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
        vars
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.tvars (PrintSpec.pp_spec m) t.tformula
243

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

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

    
273
let pp_machines = pp_print_list ~pp_open_box:pp_open_vbox0 pp_machine
274

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

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

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

    
300
let get_stateless_status m = get_stateless_status_node m.mname
301

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

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

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

    
310
let get_instr_spec i = i.instr_spec
311

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

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

    
316
let vdecls_to_vals = List.map vdecl_to_val
317

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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