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 =
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) ->
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
    | MemoryPack (f, inst, i) ->
65
      fprintf fmt "MemoryPack_%a<%a>%a"
66
        pp_print_string f
67
        (pp_print_option ~none:(fun fmt () -> pp_print_string fmt "SELF")
68
           pp_print_string) inst
69
        (pp_print_option pp_print_int) i
70
    | ResetCleared f ->
71
      fprintf fmt "ResetCleared_%a" pp_print_string f
72
    | Initialization -> ()
73

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

    
110
end
111

    
112
let pp_spec m =
113
  pp_print_list
114
    ~pp_open_box:pp_open_vbox0
115
    ~pp_prologue:pp_print_cut
116
    (fun fmt -> fprintf fmt "@[<h>--%@ %a@]" (PrintSpec.pp_spec m))
117

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

    
140
  end;
141
  (* Annotation *)
142
  (* let _ = *)
143
  (*   match i.lustre_expr with None -> () | Some e -> fprintf fmt " -- original expr: %a" Printers.pp_expr e *)
144
  (* in *)
145
  begin match i.lustre_eq with
146
  | None -> ()
147
  | Some eq -> fprintf fmt " @[<h>-- original eq: %a@]" Printers.pp_node_eq eq
148
  end;
149
  pp_spec m fmt i.instr_spec
150

    
151

    
152
and pp_branch m fmt (t, h) =
153
  fprintf fmt "@[<v 2>%s:@,%a@]" t
154
    (pp_print_list ~pp_open_box:pp_open_vbox0 (pp_instr m)) h
155

    
156
let pp_instrs m =
157
  pp_print_list ~pp_open_box:pp_open_vbox0 (pp_instr m)
158

    
159

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

    
177
let pp_step m fmt s =
178
  fprintf fmt
179
    "@[<v>\
180
     inputs : %a@ \
181
     outputs: %a@ \
182
     locals : %a@ \
183
     checks : %a@ \
184
     instrs : @[%a@]@ \
185
     asserts : @[%a@]@]@ "
186
    (pp_comma_list Printers.pp_var) s.step_inputs
187
    (pp_comma_list Printers.pp_var) s.step_outputs
188
    (pp_comma_list Printers.pp_var) s.step_locals
189
    (pp_comma_list (fun fmt (_, c) -> pp_val m fmt c))
190
    s.step_checks
191
    (pp_instrs m) s.step_instrs
192
    (pp_comma_list (pp_val m)) s.step_asserts
193

    
194
let pp_static_call fmt (node, args) =
195
  fprintf fmt "%s<%a>"
196
    (node_name node)
197
    (pp_comma_list Dimension.pp_dimension) args
198

    
199
let pp_instance fmt (o1, o2) =
200
  fprintf fmt "(%s, %a)"
201
    o1
202
    pp_static_call o2
203

    
204
let pp_memory_pack m fmt mp =
205
  fprintf fmt
206
    "@[<v 2>MemoryPack_%a<SELF>%a =@ %a@]"
207
    pp_print_string mp.mpname.node_id
208
    (pp_print_option pp_print_int) mp.mpindex
209
    (PrintSpec.pp_spec m) mp.mpformula
210

    
211
let pp_memory_packs m fmt =
212
  fprintf fmt
213
    "@[<v 2>memory_packs:@ %a@]"
214
    (pp_print_list (pp_memory_pack m))
215

    
216
let pp_transition m fmt t =
217
  fprintf fmt
218
    "@[<v 2>Transition_%a<SELF>%a%a =@ %a@]"
219
    pp_print_string t.tname.node_id
220
    (pp_print_option pp_print_int) t.tindex
221
    (pp_print_parenthesized pp_vdecl) (t.tinputs @ t.tlocals @ t.toutputs)
222
    (PrintSpec.pp_spec m) t.tformula
223

    
224
let pp_transitions m fmt =
225
  fprintf fmt
226
    "@[<v 2>transitions:@ %a@]"
227
    (pp_print_list (pp_transition m))
228

    
229
let pp_machine fmt m =
230
  fprintf fmt
231
    "@[<v 2>machine %s@ \
232
     mem      : %a@ \
233
     instances: %a@ \
234
     init     : %a@ \
235
     const    : %a@ \
236
     step     :@   \
237
     @[<v 2>%a@]@ \
238
     spec     : @[<v>%t@ %a@ @ %a@]@ \
239
     annot    : @[%a@]@]@ "
240
    m.mname.node_id
241
    (pp_comma_list Printers.pp_var) m.mmemory
242
    (pp_comma_list pp_instance) m.minstances
243
    (pp_instrs m) m.minit
244
    (pp_instrs m) m.mconst
245
    (pp_step m) m.mstep
246
    (fun fmt -> match m.mspec.mnode_spec with
247
       | None -> ()
248
       | Some (NodeSpec id) -> fprintf fmt "cocospec: %s" id
249
       | Some (Contract spec) -> Printers.pp_spec fmt spec)
250
    (pp_memory_packs m) m.mspec.mmemory_packs
251
    (pp_transitions m) m.mspec.mtransitions
252
    (pp_print_list Printers.pp_expr_annot) m.mannot
253

    
254
let pp_machines =
255
  pp_print_list ~pp_open_box:pp_open_vbox0 pp_machine
256

    
257
let rec is_const_value v =
258
  match v.value_desc with
259
  | Cst _          -> true
260
  | Fun (_, args) -> Basic_library.is_value_internal_fun v && List.for_all is_const_value args
261
  | _              -> false
262

    
263
(* Returns the declared stateless status and the computed one. *)
264
let get_stateless_status_node n =
265
  (n.node_dec_stateless,
266
   try
267
     Utils.desome n.node_stateless
268
   with _ -> failwith ("stateless status of machine " ^ n.node_id ^ " not computed"))
269

    
270
let get_stateless_status_top_decl td = match td.top_decl_desc with
271
  | Node n -> get_stateless_status_node n
272
  | ImportedNode n -> n.nodei_stateless, false
273
  | _ -> true, false
274

    
275
let get_stateless_status m =
276
  get_stateless_status_node m.mname
277

    
278
let is_stateless m = m.minstances = [] && m.mmemory = []
279

    
280
(* let is_input m id =
281
 *   List.exists (fun o -> o.var_id = id.var_id) m.mstep.step_inputs *)
282

    
283
let is_output m id =
284
  List.exists (fun o -> o.var_id = id.var_id) m.mstep.step_outputs
285

    
286
let get_instr_spec i = i.instr_spec
287

    
288
let mk_val v t =
289
  { value_desc = v;
290
    value_type = t;
291
    value_annot = None }
292

    
293
let vdecl_to_val vd =
294
  mk_val (Var vd) vd.var_type
295

    
296
let vdecls_to_vals =
297
  List.map vdecl_to_val
298

    
299
let id_to_tag id =
300
  let typ = (typedef_of_top (Hashtbl.find Corelang.tag_table id)).tydef_id in
301
  mk_val (Cst (Const_tag id)) (Type_predef.type_const typ)
302

    
303
let mk_conditional ?lustre_eq c t e =
304
  mkinstr ?lustre_eq
305
    (* (Ternary (Val c,
306
     *           And (List.map get_instr_spec t),
307
     *           And (List.map get_instr_spec e))) *)
308
    (MBranch(c, [
309
         (tag_true, t);
310
         (tag_false, e) ]))
311

    
312
let mk_branch ?lustre_eq c br =
313
  mkinstr ?lustre_eq
314
    (* (And (List.map (fun (l, instrs) ->
315
     *      Imply (Equal (Val c, Tag l), And (List.map get_instr_spec instrs)))
316
     *      br)) *)
317
    (MBranch (c, br))
318

    
319
let mk_branch' ?lustre_eq v =
320
  mk_branch ?lustre_eq (vdecl_to_val v)
321

    
322
let mk_assign ?lustre_eq x v =
323
  mkinstr ?lustre_eq
324
    (* (Equal (Var x, Val v)) *)
325
    (MLocalAssign (x, v))
326

    
327
let arrow_machine =
328
  let state = "_first" in
329
  let var_state = dummy_var_decl state Type_predef.type_bool(* (Types.new_ty Types.Tbool) *) in
330
  let var_input1 = List.nth Arrow.arrow_desc.node_inputs 0 in
331
  let var_input2 = List.nth Arrow.arrow_desc.node_inputs 1 in
332
  let var_output = List.nth Arrow.arrow_desc.node_outputs 0 in
333
  let cst b = mk_val (Cst (const_of_bool b)) Type_predef.type_bool in
334
  assert(var_input1.var_type = var_input2.var_type);
335
  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 ? *)
336
  {
337
    mname = Arrow.arrow_desc;
338
    mmemory = [var_state];
339
    mcalls = [];
340
    minstances = [];
341
    minit = [mkinstr (MStateAssign(var_state, cst true))];
342
    mstatic = [];
343
    mconst = [];
344
    mstep = {
345
      step_inputs = Arrow.arrow_desc.node_inputs;
346
      step_outputs = Arrow.arrow_desc.node_outputs;
347
      step_locals = [];
348
      step_checks = [];
349
      step_instrs = [mk_conditional (mk_val (Var var_state) Type_predef.type_bool)
350
                       (List.map mkinstr
351
                          [MStateAssign(var_state, cst false);
352
                           MLocalAssign(var_output, mk_val (Var var_input1) t_arg)])
353
                       (List.map mkinstr
354
                          [MLocalAssign(var_output, mk_val (Var var_input2) t_arg)]) ];
355
      step_asserts = [];
356
    };
357
    mspec = { mnode_spec = None; mtransitions = []; mmemory_packs = [] };
358
    mannot = [];
359
    msch = None
360
  }
361

    
362
let empty_desc =
363
  {
364
    node_id = Arrow.arrow_id;
365
    node_type = Types.bottom;
366
    node_clock = Clocks.bottom;
367
    node_inputs= [];
368
    node_outputs= [];
369
    node_locals= [];
370
    node_gencalls = [];
371
    node_checks = [];
372
    node_asserts = [];
373
    node_stmts= [];
374
    node_dec_stateless = true;
375
    node_stateless = Some true;
376
    node_spec = None;
377
    node_annot = [];
378
    node_iscontract = false;
379
}
380

    
381
let empty_machine =
382
  {
383
    mname = empty_desc;
384
    mmemory = [];
385
    mcalls = [];
386
    minstances = [];
387
    minit = [];
388
    mstatic = [];
389
    mconst = [];
390
    mstep = {
391
      step_inputs = [];
392
      step_outputs = [];
393
      step_locals = [];
394
      step_checks = [];
395
      step_instrs = [];
396
      step_asserts = [];
397
    };
398
    mspec = { mnode_spec = None; mtransitions = []; mmemory_packs = [] };
399
    mannot = [];
400
    msch = None
401
  }
402

    
403
let new_instance =
404
  let cpt = ref (-1) in
405
  fun callee tag ->
406
    begin
407
      let o =
408
	if Stateless.check_node callee then
409
	  node_name callee
410
	else
411
	  Printf.sprintf "ni_%d" (incr cpt; !cpt) in
412
      let o =
413
	if !Options.ansi && is_generic_node callee
414
	then Printf.sprintf "%s_inst_%d"
415
               o
416
               (incr cpt; !cpt)
417
	else o in
418
      o
419
    end
420

    
421

    
422
let get_machine_opt machines name =
423
  List.fold_left
424
    (fun res m ->
425
      match res with
426
      | Some _ -> res
427
      | None -> if m.mname.node_id = name then Some m else None)
428
    None machines
429

    
430
let get_machine machines node_name =
431
 try
432
    Utils.desome (get_machine_opt machines node_name) 
433
 with Utils.DeSome ->
434
   eprintf "Unable to find machine %s in machines %a@.@?"
435
     node_name
436
     (Utils.fprintf_list ~sep:", " (fun fmt m -> pp_print_string fmt m.mname.node_id)) machines
437
      ; assert false
438
     
439
let get_const_assign m id =
440
  try
441
    match get_instr_desc (List.find
442
	     (fun instr -> match get_instr_desc instr with
443
	     | MLocalAssign (v, _) -> v == id
444
	     | _ -> false)
445
	     m.mconst
446
    ) with
447
    | MLocalAssign (_, e) -> e
448
    | _                   -> assert false
449
  with Not_found -> assert false
450

    
451

    
452
let value_of_ident loc m id =
453
  (* is is a state var *)
454
  try
455
    let v = List.find (fun v -> v.var_id = id) m.mmemory
456
    in mk_val (Var v) v.var_type 
457
  with Not_found ->
458
    try (* id is a node var *)
459
      let v = get_node_var id m.mname
460
      in mk_val (Var v) v.var_type
461
  with Not_found ->
462
    try (* id is a constant *)
463
      let c = Corelang.var_decl_of_const (const_of_top (Hashtbl.find Corelang.consts_table id))
464
      in mk_val (Var c) c.var_type
465
    with Not_found ->
466
      (* id is a tag *)
467
      let t = Const_tag id
468
      in mk_val (Cst t) (Typing.type_const loc t)
469

    
470
(* type of internal fun used in dimension expression *)
471
let type_of_value_appl f args =
472
  if List.mem f Basic_library.arith_funs
473
  then (List.hd args).value_type
474
  else Type_predef.type_bool
475

    
476
let rec value_of_dimension m dim =
477
  match dim.Dimension.dim_desc with
478
  | Dimension.Dbool b         ->
479
     mk_val (Cst (Const_tag (if b then tag_true else tag_false))) Type_predef.type_bool
480
  | Dimension.Dint i          ->
481
     mk_val (Cst (Const_int i)) Type_predef.type_int
482
  | Dimension.Dident v        -> value_of_ident dim.Dimension.dim_loc m v
483
  | Dimension.Dappl (f, args) ->
484
     let vargs = List.map (value_of_dimension m) args
485
     in mk_val (Fun (f, vargs)) (type_of_value_appl f vargs) 
486
  | Dimension.Dite (i, t, e)  ->
487
     (match List.map (value_of_dimension m) [i; t; e] with
488
     | [vi; vt; ve] -> mk_val (Fun ("ite", [vi; vt; ve])) vt.value_type
489
     | _            -> assert false)
490
  | Dimension.Dlink dim'      -> value_of_dimension m dim'
491
  | _                         -> assert false
492

    
493
let rec dimension_of_value value =
494
  match value.value_desc with
495
  | Cst (Const_tag t) when t = tag_true  -> Dimension.mkdim_bool  Location.dummy_loc true
496
  | Cst (Const_tag t) when t = tag_false -> Dimension.mkdim_bool  Location.dummy_loc false
497
  | Cst (Const_int i)                             -> Dimension.mkdim_int   Location.dummy_loc i
498
  | Var v                                         -> Dimension.mkdim_ident Location.dummy_loc v.var_id
499
  | Fun (f, args)                                 -> Dimension.mkdim_appl  Location.dummy_loc f (List.map dimension_of_value args)
500
  | _                                             -> assert false
501

    
502

    
503
let rec join_branches hl1 hl2 =
504
 match hl1, hl2 with
505
 | []          , _            -> hl2
506
 | _           , []           -> hl1
507
 | (t1, h1)::q1, (t2, h2)::q2 ->
508
   if t1 < t2 then (t1, h1) :: join_branches q1 hl2 else
509
   if t1 > t2 then (t2, h2) :: join_branches hl1 q2
510
   else (t1, List.fold_right join_guards h1 h2) :: join_branches q1 q2
511

    
512
and join_guards inst1 insts2 =
513
 match get_instr_desc inst1, insts2 with
514
   | MBranch (x1, hl1),
515
     ({ instr_desc = MBranch (x2, hl2); _ } as inst2) :: insts2
516
     when x1 = x2 ->
517
     mkinstr
518
       ~instr_spec:(get_instr_spec inst1 @ get_instr_spec inst2)
519
       (* TODO on pourrait uniquement concatener les lustres de inst1 et hd(inst2) *)
520
       (MBranch (x1, join_branches (sort_handlers hl1) (sort_handlers hl2)))
521
     :: insts2
522
   | _ -> inst1 :: insts2
523

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