Project

General

Profile

Download (16.6 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 =
10
  (List.exists (fun o -> o.var_id = id.var_id) m.mmemory) 
11

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

    
15
let pp_vdecl fmt v =
16
  pp_print_string fmt v.var_id
17

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

    
39
module PrintSpec = struct
40

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

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

    
52
  let pp_predicate m fmt p =
53
    let pp_expr: type a. formatter -> (value_t, a) expression_t -> unit =
54
      fun fmt e -> pp_expr m fmt e
55
    in
56
    match p with
57
    | Transition (f, inst, i, inputs, locals, outputs, _r, _mems) ->
58
      fprintf fmt "Transition_%a<%a>%a%a"
59
        pp_print_string f
60
        (pp_print_option ~none:(fun fmt () -> pp_print_string fmt "SELF")
61
           pp_print_string) inst
62
        (pp_print_option pp_print_int) i
63
        (pp_print_parenthesized pp_expr) (inputs @ locals @ outputs)
64
    | Reset (f, inst, r) ->
65
      fprintf fmt "Reset_%a<%a> on %a"
66
        pp_print_string f
67
        pp_print_string inst
68
        (pp_val m) r
69
    | MemoryPack (f, inst, i) ->
70
      fprintf fmt "MemoryPack_%a<%a>%a"
71
        pp_print_string f
72
        (pp_print_option ~none:(fun fmt () -> pp_print_string fmt "SELF")
73
           pp_print_string) inst
74
        (pp_print_option pp_print_int) i
75
    | ResetCleared f ->
76
      fprintf fmt "ResetCleared_%a" pp_print_string f
77
    | Initialization -> ()
78

    
79
  let pp_spec m =
80
    let pp_expr: type a. formatter -> (value_t, a) expression_t -> unit =
81
      fun fmt e -> pp_expr m fmt e
82
    in
83
    let rec pp_spec fmt f =
84
      match f with
85
      | True -> pp_print_string fmt "true"
86
      | False -> pp_print_string fmt "false"
87
      | Equal (a, b) ->
88
        fprintf fmt "%a == %a" pp_expr a pp_expr b
89
      | And fs ->
90
        pp_print_list ~pp_sep:(fun fmt () -> fprintf fmt "@ ∧ ")
91
          (fun fmt spec -> fprintf fmt "@[%a@]" pp_spec spec) fmt fs
92
      | Or fs ->
93
        pp_print_list ~pp_sep:(fun fmt () -> fprintf fmt "@ ∨ ")
94
          (fun fmt spec -> fprintf fmt "@[%a@]" pp_spec spec) fmt fs
95
      | Imply (a, b) ->
96
        fprintf fmt "%a@ -> %a" pp_spec a pp_spec b
97
      | Exists (xs, a) ->
98
        fprintf fmt "@[<hv 2>∃ @[<h>%a,@]@ %a@]"
99
          (pp_comma_list Printers.pp_var) xs pp_spec a
100
      | Forall (xs, a) ->
101
        fprintf fmt "@[<hv 2>∀ @[<h>%a,@]@ %a@]"
102
          (pp_comma_list Printers.pp_var) xs pp_spec a
103
      | Ternary (e, a, b) ->
104
        fprintf fmt "If %a Then (@[<hov>%a@]) Else (@[<hov>%a@])"
105
          pp_expr e pp_spec a pp_spec b
106
      | Predicate p ->
107
        pp_predicate m fmt p
108
      | StateVarPack r ->
109
        fprintf fmt "StateVarPack<%a>" pp_reg r
110
      | ExistsMem (_f, a, b) ->
111
        fprintf fmt "@[<hv 2>∃ MEM,@ %a@]" pp_spec (And [a; b])
112
    in
113
    pp_spec
114

    
115
end
116

    
117
let pp_spec m =
118
  if !Options.spec <> "no" then
119
    pp_print_list
120
      ~pp_open_box:pp_open_vbox0
121
      ~pp_prologue:pp_print_cut
122
      (fun fmt -> fprintf fmt "@[<h>--%@ %a@]" (PrintSpec.pp_spec m))
123
  else
124
    pp_print_nothing
125

    
126
let rec pp_instr m fmt i =
127
  let pp_val = pp_val m in
128
  let pp_branch = pp_branch m in
129
  begin match i.instr_desc with
130
    | MLocalAssign (i,v) -> fprintf fmt "%s := %a" i.var_id pp_val v
131
    | MStateAssign (i,v) -> fprintf fmt "{%s} := %a" i.var_id pp_val v
132
    | MResetAssign b     -> fprintf fmt "RESET := %a" pp_print_bool b
133
    | MSetReset i        -> fprintf fmt "set_reset %s" i
134
    | MClearReset        -> fprintf fmt "clear_reset %s" m.mname.node_id
135
    | MNoReset i         -> fprintf fmt "noreset %s" i
136
    | MStep (il, i, vl)  ->
137
      fprintf fmt "%a := %s%a"
138
        (pp_comma_list pp_vdecl) il
139
        i
140
        (pp_print_parenthesized pp_val) vl
141
    | MBranch (g,hl)     ->
142
      fprintf fmt "@[<v 2>case(%a) {@,%a@]@,}"
143
        pp_val g
144
        (pp_print_list ~pp_open_box:pp_open_vbox0 pp_branch) hl
145
    | MComment s -> pp_print_string fmt s
146
    | MSpec s -> pp_print_string fmt ("@" ^ s)
147

    
148
  end;
149
  (* Annotation *)
150
  (* let _ = *)
151
  (*   match i.lustre_expr with None -> () | Some e -> fprintf fmt " -- original expr: %a" Printers.pp_expr e *)
152
  (* in *)
153
  begin match i.lustre_eq with
154
  | None -> ()
155
  | Some eq -> fprintf fmt " @[<h>-- original eq: %a@]" Printers.pp_node_eq eq
156
  end;
157
  pp_spec m fmt i.instr_spec
158

    
159

    
160
and pp_branch m fmt (t, h) =
161
  fprintf fmt "@[<v 2>%s:@,%a@]" t
162
    (pp_print_list ~pp_open_box:pp_open_vbox0 (pp_instr m)) h
163

    
164
let pp_instrs m =
165
  pp_print_list ~pp_open_box:pp_open_vbox0 (pp_instr m)
166

    
167

    
168
(* merge log: get_node_def was in c0f8 *)
169
(* Returns the node/machine associated to id in m calls *)
170
let get_node_def id m =
171
  try
172
    let (decl, _) = List.assoc id m.mcalls in
173
    Corelang.node_of_top decl
174
  with Not_found -> ( 
175
    (* eprintf "Unable to find node %s in list [%a]@.@?" *)
176
    (*   id *)
177
    (*   (Utils.fprintf_list ~sep:", " (fun fmt (n,_) -> fprintf fmt "%s" n)) m.mcalls *)
178
    (* ; *)
179
    raise Not_found
180
  )
181
    
182
(* merge log: machine_vars was in 44686 *)
183
let machine_vars m = m.mstep.step_inputs @ m.mstep.step_locals @ m.mstep.step_outputs @ m.mmemory
184

    
185
let pp_step m fmt s =
186
  fprintf fmt
187
    "@[<v>\
188
     inputs : %a@ \
189
     outputs: %a@ \
190
     locals : %a@ \
191
     checks : %a@ \
192
     instrs : @[%a@]@ \
193
     asserts : @[%a@]@]@ "
194
    (pp_comma_list Printers.pp_var) s.step_inputs
195
    (pp_comma_list Printers.pp_var) s.step_outputs
196
    (pp_comma_list Printers.pp_var) s.step_locals
197
    (pp_comma_list (fun fmt (_, c) -> pp_val m fmt c))
198
    s.step_checks
199
    (pp_instrs m) s.step_instrs
200
    (pp_comma_list (pp_val m)) s.step_asserts
201

    
202
let pp_static_call fmt (node, args) =
203
  fprintf fmt "%s<%a>"
204
    (node_name node)
205
    (pp_comma_list Dimension.pp_dimension) args
206

    
207
let pp_instance fmt (o1, o2) =
208
  fprintf fmt "(%s, %a)"
209
    o1
210
    pp_static_call o2
211

    
212
let pp_memory_pack m fmt mp =
213
  fprintf fmt
214
    "@[<v 2>MemoryPack_%a<SELF>%a =@ %a@]"
215
    pp_print_string mp.mpname.node_id
216
    (pp_print_option pp_print_int) mp.mpindex
217
    (PrintSpec.pp_spec m) mp.mpformula
218

    
219
let pp_memory_packs m fmt =
220
  if !Options.spec <> "no" then
221
    fprintf fmt
222
      "@[<v 2>memory_packs:@ %a@]"
223
      (pp_print_list (pp_memory_pack m))
224
  else
225
    pp_print_nothing fmt
226

    
227
let pp_transition m fmt t =
228
  fprintf fmt
229
    "@[<v 2>Transition_%a<SELF>%a%a =@ %a@]"
230
    pp_print_string t.tname.node_id
231
    (pp_print_option pp_print_int) t.tindex
232
    (pp_print_parenthesized pp_vdecl) (t.tinputs @ t.tlocals @ t.toutputs)
233
    (PrintSpec.pp_spec m) t.tformula
234

    
235
let pp_transitions m fmt =
236
  if !Options.spec <> "no" then
237
    fprintf fmt
238
      "@[<v 2>transitions:@ %a@]"
239
      (pp_print_list (pp_transition m))
240
  else
241
    pp_print_nothing fmt
242

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

    
268
let pp_machines =
269
  pp_print_list ~pp_open_box:pp_open_vbox0 pp_machine
270

    
271
let rec is_const_value v =
272
  match v.value_desc with
273
  | Cst _          -> true
274
  | Fun (_, args) -> Basic_library.is_value_internal_fun v && List.for_all is_const_value args
275
  | _              -> false
276

    
277
(* Returns the declared stateless status and the computed one. *)
278
let get_stateless_status_node n =
279
  (n.node_dec_stateless,
280
   try
281
     Utils.desome n.node_stateless
282
   with _ -> failwith ("stateless status of machine " ^ n.node_id ^ " not computed"))
283

    
284
let get_stateless_status_top_decl td = match td.top_decl_desc with
285
  | Node n -> get_stateless_status_node n
286
  | ImportedNode n -> n.nodei_stateless, false
287
  | _ -> true, false
288

    
289
let get_stateless_status m =
290
  get_stateless_status_node m.mname
291

    
292
let is_stateless m = m.minstances = [] && m.mmemory = []
293

    
294
(* let is_input m id =
295
 *   List.exists (fun o -> o.var_id = id.var_id) m.mstep.step_inputs *)
296

    
297
let is_output m id =
298
  List.exists (fun o -> o.var_id = id.var_id) m.mstep.step_outputs
299

    
300
let get_instr_spec i = i.instr_spec
301

    
302
let mk_val v t =
303
  { value_desc = v;
304
    value_type = t;
305
    value_annot = None }
306

    
307
let vdecl_to_val vd =
308
  mk_val (Var vd) vd.var_type
309

    
310
let vdecls_to_vals =
311
  List.map vdecl_to_val
312

    
313
let id_to_tag id =
314
  let typ = (typedef_of_top (Hashtbl.find Corelang.tag_table id)).tydef_id in
315
  mk_val (Cst (Const_tag id)) (Type_predef.type_const typ)
316

    
317
let mk_conditional ?lustre_eq c t e =
318
  mkinstr ?lustre_eq
319
    (* (Ternary (Val c,
320
     *           And (List.map get_instr_spec t),
321
     *           And (List.map get_instr_spec e))) *)
322
    (MBranch(c, [
323
         (tag_true, t);
324
         (tag_false, e) ]))
325

    
326
let mk_branch ?lustre_eq c br =
327
  mkinstr ?lustre_eq
328
    (* (And (List.map (fun (l, instrs) ->
329
     *      Imply (Equal (Val c, Tag l), And (List.map get_instr_spec instrs)))
330
     *      br)) *)
331
    (MBranch (c, br))
332

    
333
let mk_branch' ?lustre_eq v =
334
  mk_branch ?lustre_eq (vdecl_to_val v)
335

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

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

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

    
395
let empty_machine =
396
  {
397
    mname = empty_desc;
398
    mmemory = [];
399
    mcalls = [];
400
    minstances = [];
401
    minit = [];
402
    mstatic = [];
403
    mconst = [];
404
    mstep = {
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
    begin
421
      let o =
422
	if Stateless.check_node callee then
423
	  node_name callee
424
	else
425
	  Printf.sprintf "ni_%d" (incr cpt; !cpt) in
426
      let o =
427
	if !Options.ansi && is_generic_node callee
428
	then Printf.sprintf "%s_inst_%d"
429
               o
430
               (incr cpt; !cpt)
431
	else o in
432
      o
433
    end
434

    
435

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

    
444
let get_machine machines node_name =
445
 try
446
    Utils.desome (get_machine_opt machines node_name) 
447
 with Utils.DeSome ->
448
   eprintf "Unable to find machine %s in machines %a@.@?"
449
     node_name
450
     (Utils.fprintf_list ~sep:", " (fun fmt m -> pp_print_string fmt m.mname.node_id)) machines
451
      ; assert false
452
     
453
let get_const_assign m id =
454
  try
455
    match get_instr_desc (List.find
456
	     (fun instr -> match get_instr_desc instr with
457
	     | MLocalAssign (v, _) -> v == id
458
	     | _ -> false)
459
	     m.mconst
460
    ) with
461
    | MLocalAssign (_, e) -> e
462
    | _                   -> assert false
463
  with Not_found -> assert false
464

    
465

    
466
let value_of_ident loc m id =
467
  (* is is a state var *)
468
  try
469
    let v = List.find (fun v -> v.var_id = id) m.mmemory
470
    in mk_val (Var v) v.var_type 
471
  with Not_found ->
472
    try (* id is a node var *)
473
      let v = get_node_var id m.mname
474
      in mk_val (Var v) v.var_type
475
  with Not_found ->
476
    try (* id is a constant *)
477
      let c = Corelang.var_decl_of_const (const_of_top (Hashtbl.find Corelang.consts_table id))
478
      in mk_val (Var c) c.var_type
479
    with Not_found ->
480
      (* id is a tag *)
481
      let t = Const_tag id
482
      in mk_val (Cst t) (Typing.type_const loc t)
483

    
484
(* type of internal fun used in dimension expression *)
485
let type_of_value_appl f args =
486
  if List.mem f Basic_library.arith_funs
487
  then (List.hd args).value_type
488
  else Type_predef.type_bool
489

    
490
let rec value_of_dimension m dim =
491
  match dim.Dimension.dim_desc with
492
  | Dimension.Dbool b         ->
493
     mk_val (Cst (Const_tag (if b then tag_true else tag_false))) Type_predef.type_bool
494
  | Dimension.Dint i          ->
495
     mk_val (Cst (Const_int i)) Type_predef.type_int
496
  | Dimension.Dident v        -> value_of_ident dim.Dimension.dim_loc m v
497
  | Dimension.Dappl (f, args) ->
498
     let vargs = List.map (value_of_dimension m) args
499
     in mk_val (Fun (f, vargs)) (type_of_value_appl f vargs) 
500
  | Dimension.Dite (i, t, e)  ->
501
     (match List.map (value_of_dimension m) [i; t; e] with
502
     | [vi; vt; ve] -> mk_val (Fun ("ite", [vi; vt; ve])) vt.value_type
503
     | _            -> assert false)
504
  | Dimension.Dlink dim'      -> value_of_dimension m dim'
505
  | _                         -> assert false
506

    
507
let rec dimension_of_value value =
508
  match value.value_desc with
509
  | Cst (Const_tag t) when t = tag_true  -> Dimension.mkdim_bool  Location.dummy_loc true
510
  | Cst (Const_tag t) when t = tag_false -> Dimension.mkdim_bool  Location.dummy_loc false
511
  | Cst (Const_int i)                             -> Dimension.mkdim_int   Location.dummy_loc i
512
  | Var v                                         -> Dimension.mkdim_ident Location.dummy_loc v.var_id
513
  | Fun (f, args)                                 -> Dimension.mkdim_appl  Location.dummy_loc f (List.map dimension_of_value args)
514
  | _                                             -> assert false
515

    
516

    
517
let rec join_branches hl1 hl2 =
518
 match hl1, hl2 with
519
 | []          , _            -> hl2
520
 | _           , []           -> hl1
521
 | (t1, h1)::q1, (t2, h2)::q2 ->
522
   if t1 < t2 then (t1, h1) :: join_branches q1 hl2 else
523
   if t1 > t2 then (t2, h2) :: join_branches hl1 q2
524
   else (t1, List.fold_right join_guards h1 h2) :: join_branches q1 q2
525

    
526
and join_guards inst1 insts2 =
527
 match get_instr_desc inst1, insts2 with
528
   | MBranch (x1, hl1),
529
     ({ instr_desc = MBranch (x2, hl2); _ } as inst2) :: insts2
530
     when x1 = x2 ->
531
     mkinstr
532
       ~instr_spec:(get_instr_spec inst1 @ get_instr_spec inst2)
533
       (* TODO on pourrait uniquement concatener les lustres de inst1 et hd(inst2) *)
534
       (MBranch (x1, join_branches (sort_handlers hl1) (sort_handlers hl2)))
535
     :: insts2
536
   | _ -> inst1 :: insts2
537

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