Project

General

Profile

Download (16.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.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

    
38
module PrintSpec = struct
39

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

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

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

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

    
109
end
110

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

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

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

    
149

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

    
154
let pp_instrs m =
155
  pp_print_list ~pp_open_box:pp_open_vbox0 (pp_instr m)
156

    
157

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

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

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

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

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

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

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

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

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

    
252
let pp_machines =
253
  pp_print_list ~pp_open_box:pp_open_vbox0 pp_machine
254

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

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

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

    
273
let get_stateless_status m =
274
  get_stateless_status_node m.mname
275

    
276
let is_stateless m = m.minstances = [] && m.mmemory = []
277

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

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

    
284
let get_instr_spec i = i.instr_spec
285

    
286
let mk_val v t =
287
  { value_desc = v;
288
    value_type = t;
289
    value_annot = None }
290

    
291
let vdecl_to_val vd =
292
  mk_val (Var vd) vd.var_type
293

    
294
let vdecls_to_vals =
295
  List.map vdecl_to_val
296

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

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

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

    
317
let mk_assign ?lustre_eq x v =
318
  mkinstr ?lustre_eq
319
    (* (Equal (Var x, Val v)) *)
320
    (MLocalAssign (x, v))
321

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

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

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

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

    
416

    
417
let get_machine_opt machines name =
418
  List.fold_left
419
    (fun res m ->
420
      match res with
421
      | Some _ -> res
422
      | None -> if m.mname.node_id = name then Some m else None)
423
    None machines
424

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

    
446

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

    
465
(* type of internal fun used in dimension expression *)
466
let type_of_value_appl f args =
467
  if List.mem f Basic_library.arith_funs
468
  then (List.hd args).value_type
469
  else Type_predef.type_bool
470

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

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

    
497

    
498
let rec join_branches hl1 hl2 =
499
 match hl1, hl2 with
500
 | []          , _            -> hl2
501
 | _           , []           -> hl1
502
 | (t1, h1)::q1, (t2, h2)::q2 ->
503
   if t1 < t2 then (t1, h1) :: join_branches q1 hl2 else
504
   if t1 > t2 then (t2, h2) :: join_branches hl1 q2
505
   else (t1, List.fold_right join_guards h1 h2) :: join_branches q1 q2
506

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

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