Project

General

Profile

Download (24.9 KB) Statistics
| Branch: | Tag: | Revision:
1
(*                                                                  *)
2
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
3
(*  Copyright 2012 -    --   ONERA - CNRS - INPT                    *)
4
(*                                                                  *)
5
(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
6
(*  under the terms of the GNU Lesser General Public License        *)
7
(*  version 2.1.                                                    *)
8
(*                                                                  *)
9
(********************************************************************)
10

    
11
(* The compilation presented here is defined in Garoche, Gurfinkel, Kahsai,
12
   HCSV'14 *)
13

    
14
open Format
15
open LustreSpec
16
open Corelang
17
open Machine_code
18

    
19

    
20
let pp_machine_init_name fmt id = fprintf fmt "%s_init" id
21
let pp_machine_step_name fmt id = fprintf fmt "%s_step" id
22
let pp_machine_stateless_name fmt id = fprintf fmt "%s" id
23

    
24
let pp_type fmt t =
25
  match (Types.repr t).Types.tdesc with
26
  | Types.Tbool           -> Format.fprintf fmt "Bool"
27
  | Types.Tint            -> Format.fprintf fmt "Int"
28
  | Types.Treal           -> Format.fprintf fmt "Real"
29
  | Types.Tclock _
30
  | Types.Tarray _
31
  | Types.Tstatic _
32
  | Types.Tconst _
33
  | Types.Tarrow _
34
  | _                     -> Format.eprintf "internal error: pp_type %a@."
35
    Types.print_ty t; assert false
36

    
37
let pp_decl_var fmt id =
38
  Format.fprintf fmt "(declare-var %s %a)"
39
    id.var_id
40
    pp_type id.var_type
41

    
42
let pp_var fmt id = Format.pp_print_string fmt id.var_id
43

    
44

    
45
let pp_conj pp fmt l =
46
  match l with
47
    [] -> assert false
48
  | [x] -> pp fmt x
49
  | _ -> fprintf fmt "(and @[<v 0>%a@]@ )" (Utils.fprintf_list ~sep:" " pp) l
50

    
51

    
52

    
53
let concat prefix x = if prefix = "" then x else prefix ^ "." ^ x
54
let rename f = (fun v -> {v with var_id = f v.var_id } )
55
let rename_machine p = rename (fun n -> concat p n)
56
let rename_machine_list p = List.map (rename_machine p)
57

    
58
let rename_current =  rename (fun n -> n ^ "_c")
59
let rename_current_list = List.map rename_current
60
let rename_next = rename (fun n -> n ^ "_x")
61
let rename_next_list = List.map rename_next
62

    
63

    
64
let get_machine machines node_name =
65
  List.find (fun m  -> m.mname.node_id = node_name) machines
66

    
67

    
68
let full_memory_vars machines machine =
69
  let rec aux fst prefix m =
70
    (rename_machine_list (if fst then prefix else concat prefix m.mname.node_id) m.mmemory) @
71
      List.fold_left (fun accu (id, (n, _)) ->
72
	let name = node_name n in
73
	if name = "_arrow" then accu else
74
	  let machine_n = get_machine machines name in
75
	  ( aux false (concat prefix (if fst then id else concat m.mname.node_id id)) machine_n ) @ accu
76
      ) [] (m.minstances)
77
  in
78
  aux true machine.mname.node_id machine
79

    
80

    
81
let stateless_vars machines m =
82
  (rename_machine_list m.mname.node_id m.mstep.step_inputs)@
83
    (rename_machine_list m.mname.node_id m.mstep.step_outputs)
84

    
85
let step_vars machines m =
86
  (stateless_vars machines m)@
87
    (rename_current_list (full_memory_vars machines m)) @
88
    (rename_next_list (full_memory_vars machines m))
89

    
90
let init_vars machines m =
91
  (stateless_vars machines m) @ (rename_next_list (full_memory_vars machines m))
92

    
93
(********************************************************************************************)
94
(*                    Instruction Printing functions                                        *)
95
(********************************************************************************************)
96

    
97
let pp_horn_var m fmt id =
98
  if Types.is_array_type id.var_type
99
  then
100
    assert false (* no arrays in Horn output *)
101
  else
102
    Format.fprintf fmt "%s" id.var_id
103

    
104

    
105
(* Used to print boolean constants *)
106
let pp_horn_tag fmt t =
107
  pp_print_string fmt (if t = tag_true then "true" else if t = tag_false then "false" else t)
108

    
109
(* Prints a constant value *)
110
let rec pp_horn_const fmt c =
111
  match c with
112
    | Const_int i    -> pp_print_int fmt i
113
    | Const_real r   -> pp_print_string fmt r
114
    | Const_float r  -> pp_print_float fmt r
115
    | Const_tag t    -> pp_horn_tag fmt t
116
    | _              -> assert false
117

    
118
(* Prints a value expression [v], with internal function calls only.
119
   [pp_var] is a printer for variables (typically [pp_c_var_read]),
120
   but an offset suffix may be added for array variables
121
*)
122
let rec pp_horn_val ?(is_lhs=false) self pp_var fmt v =
123
  match v with
124
    | Cst c         -> pp_horn_const fmt c
125
    | Array _
126
    | Access _ -> assert false (* no arrays *)
127
    | Power (v, n)  -> assert false
128
    | LocalVar v    -> pp_var fmt (rename_machine self v)
129
    | StateVar v    ->
130
      if Types.is_array_type v.var_type
131
      then assert false
132
      else pp_var fmt (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v))
133
    | Fun (n, vl)   -> Format.fprintf fmt "%a" (Basic_library.pp_horn n (pp_horn_val self pp_var)) vl
134

    
135
(* Prints a [value] indexed by the suffix list [loop_vars] *)
136
let rec pp_value_suffix self pp_value fmt value =
137
 match value with
138
 | Fun (n, vl)  ->
139
   Basic_library.pp_horn n (pp_value_suffix self pp_value) fmt vl
140
 |  _            ->
141
   pp_horn_val self pp_value fmt value
142

    
143
(* type_directed assignment: array vs. statically sized type
144
   - [var_type]: type of variable to be assigned
145
   - [var_name]: name of variable to be assigned
146
   - [value]: assigned value
147
   - [pp_var]: printer for variables
148
*)
149
let pp_assign m self pp_var fmt var_type var_name value =
150
  fprintf fmt "(= %a %a)" (pp_horn_val ~is_lhs:true self pp_var) var_name (pp_value_suffix self pp_var) value
151

    
152
let pp_instance_call
153
    machines ?(init=false) m self fmt i (inputs: value_t list) (outputs: var_decl list) =
154
  try (* stateful node instance *)
155
    begin
156
      let (n,_) = List.assoc i m.minstances in
157
      match node_name n, inputs, outputs with
158
      | "_arrow", [i1; i2], [o] -> begin
159
        if init then
160
          pp_assign
161
   	    m
162
   	    self
163
   	    (pp_horn_var m)
164
	    fmt
165
   	    o.var_type (LocalVar o) i1
166
        else
167
          pp_assign
168
   	    m self (pp_horn_var m) fmt
169
   	    o.var_type (LocalVar o) i2
170

    
171
      end
172
      | name, _, _ ->
173
	begin
174
	  let target_machine = List.find (fun m  -> m.mname.node_id = name) machines in
175
	  if init then
176
	    Format.fprintf fmt "(%a %a%t%a%t%a)"
177
	      pp_machine_init_name (node_name n)
178
	      (* inputs *)
179
	      (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m)))
180
	      inputs
181
	      (Utils.pp_final_char_if_non_empty " " inputs)
182
	      (* outputs *)
183
	      (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m)))
184
	      (List.map (fun v -> LocalVar v) outputs)
185
	      (Utils.pp_final_char_if_non_empty " " outputs)
186
	      (* memories (next) *)
187
	      (Utils.fprintf_list ~sep:" " pp_var) (
188
  		rename_machine_list
189
		  (concat m.mname.node_id i)
190
		  (rename_next_list (full_memory_vars machines target_machine)
191
		  )
192
	       )
193
	  else
194
	    Format.fprintf fmt "(%a %a%t%a%t%a)"
195
	      pp_machine_step_name (node_name n)
196
	      (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) inputs
197
	      (Utils.pp_final_char_if_non_empty " " inputs)
198
	      (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m)))
199
	      (List.map (fun v -> LocalVar v) outputs)
200
	      (Utils.pp_final_char_if_non_empty " " outputs)
201
	      (Utils.fprintf_list ~sep:" " pp_var) (
202
		(rename_machine_list
203
		   (concat m.mname.node_id i)
204
		   (rename_current_list (full_memory_vars machines target_machine))
205
		) @
206
		  (rename_machine_list
207
		     (concat m.mname.node_id i)
208
		     (rename_next_list (full_memory_vars machines target_machine))
209
		  )
210
	       )
211

    
212
	end
213
    end
214
    with Not_found -> ( (* stateless node instance *)
215
      let (n,_) = List.assoc i m.mcalls in
216
      Format.fprintf fmt "(%s %a%t%a)"
217
	(node_name n)
218
	(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m)))
219
	inputs
220
	(Utils.pp_final_char_if_non_empty " " inputs)
221
	(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m)))
222
	(List.map (fun v -> LocalVar v) outputs)
223
    )
224

    
225
let pp_machine_init (m: machine_t) self fmt inst =
226
  let (node, static) = List.assoc inst m.minstances in
227
  fprintf fmt "(%a %a%t%s->%s)"
228
    pp_machine_init_name (node_name node)
229
    (Utils.fprintf_list ~sep:" " Dimension.pp_dimension) static
230
    (Utils.pp_final_char_if_non_empty " " static)
231
    self inst
232

    
233
(* TODO *)
234
let rec pp_conditional machines ?(init=false)  (m: machine_t) self fmt c tl el =
235
  fprintf fmt "@[<v 2>if (%a) {%t%a@]@,@[<v 2>} else {%t%a@]@,}"
236
    (pp_horn_val self (pp_horn_var m)) c
237
    (Utils.pp_newline_if_non_empty tl)
238
    (Utils.fprintf_list ~sep:"@," (pp_machine_instr machines ~init:init  m self)) tl
239
    (Utils.pp_newline_if_non_empty el)
240
    (Utils.fprintf_list ~sep:"@," (pp_machine_instr machines ~init:init  m self)) el
241

    
242
and pp_machine_instr machines ?(init=false) (m: machine_t) self fmt instr =
243
  match instr with
244
  | MReset i ->
245
    pp_machine_init m self fmt i
246
  | MLocalAssign (i,v) ->
247
    pp_assign
248
      m self (pp_horn_var m) fmt
249
      i.var_type (LocalVar i) v
250
  | MStateAssign (i,v) ->
251
    pp_assign
252
      m self (pp_horn_var m) fmt
253
      i.var_type (StateVar i) v
254
  | MStep ([i0], i, vl) when Basic_library.is_internal_fun i  ->
255
    assert false (* This should not happen anymore *)
256
  | MStep (il, i, vl) ->
257
    pp_instance_call machines ~init:init m self fmt i vl il
258
  | MBranch (g,hl) ->
259
    if hl <> [] && let t = fst (List.hd hl) in t = tag_true || t = tag_false
260
    then (* boolean case, needs special treatment in C because truth value is not unique *)
261
      (* may disappear if we optimize code by replacing last branch test with default *)
262
      let tl = try List.assoc tag_true  hl with Not_found -> [] in
263
      let el = try List.assoc tag_false hl with Not_found -> [] in
264
      pp_conditional machines ~init:init m self fmt g tl el
265
    else assert false (* enum type case *)
266

    
267

    
268
(**************************************************************)
269

    
270
let is_stateless m = m.minstances = [] && m.mmemory = []
271

    
272
(* Print the machine m:
273
   two functions: m_init and m_step
274
   - m_init is a predicate over m memories
275
   - m_step is a predicate over old_memories, inputs, new_memories, outputs
276
   We first declare all variables then the two /rules/.
277
*)
278
let print_machine machines fmt m =
279
  let pp_instr init = pp_machine_instr machines ~init:init m in
280
  if m.mname.node_id = arrow_id then
281
    (* We don't print arrow function *)
282
    ()
283
  else
284
    begin
285
      Format.fprintf fmt "; %s@." m.mname.node_id;
286

    
287
   (* Printing variables *)
288
   Utils.fprintf_list ~sep:"@." pp_decl_var fmt
289
     ((step_vars machines m)@
290
	 (rename_machine_list m.mname.node_id m.mstep.step_locals));
291
   Format.pp_print_newline fmt ();
292

    
293

    
294

    
295
   if is_stateless m then
296
     begin
297
       (* Declaring single predicate *)
298
       Format.fprintf fmt "(declare-rel %a (%a))@."
299
	 pp_machine_stateless_name m.mname.node_id
300
	 (Utils.fprintf_list ~sep:" " pp_type)
301
	 (List.map (fun v -> v.var_type) (stateless_vars machines m));
302

    
303
       (* Rule for single predicate *)
304
       Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@."
305
	 (pp_conj (pp_instr
306
		     true (* In this case, the boolean init can be set to true or false.
307
			     The node is stateless. *)
308
		     m.mname.node_id)
309
	 )
310
	 m.mstep.step_instrs
311
	 pp_machine_stateless_name m.mname.node_id
312
	 (Utils.fprintf_list ~sep:" " pp_var) (stateless_vars machines m);
313
     end
314
   else
315
     begin
316
       (* Declaring predicate *)
317
       Format.fprintf fmt "(declare-rel %a (%a))@."
318
	 pp_machine_init_name m.mname.node_id
319
	 (Utils.fprintf_list ~sep:" " pp_type)
320
	 (List.map (fun v -> v.var_type) (init_vars machines m));
321

    
322
       Format.fprintf fmt "(declare-rel %a (%a))@."
323
	 pp_machine_step_name m.mname.node_id
324
	 (Utils.fprintf_list ~sep:" " pp_type)
325
	 (List.map (fun v -> v.var_type) (step_vars machines m));
326

    
327
       Format.pp_print_newline fmt ();
328

    
329
       (* Rule for init *)
330
       Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@."
331
	 (pp_conj (pp_instr true m.mname.node_id)) m.mstep.step_instrs
332
	 pp_machine_init_name m.mname.node_id
333
	 (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m);
334

    
335
      (* Adding assertions *)
336
       (match m.mstep.step_asserts with
337
       | [] ->
338
          begin
339
            (* Rule for init *)
340
            Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@."
341
	                   (pp_conj (pp_instr true m.mname.node_id)) m.mstep.step_instrs
342
	                   pp_machine_init_name m.mname.node_id
343
	                   (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m);
344
            (* Rule for step*)
345
            Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@."
346
                           (pp_conj (pp_instr false m.mname.node_id)) m.mstep.step_instrs
347
                           pp_machine_step_name m.mname.node_id
348
                           (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m);
349
          end
350
       | assertsl ->
351
          begin
352
	    let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id pp_var in
353
            (* print_string pp_val; *)
354
            let instrs_concat = m.mstep.step_instrs in
355
            Format.fprintf fmt "; with Assertions @.";
356
            (*Rule for init*)
357
            Format.fprintf fmt "@[<v 2>(rule (=> @ (and @ %a@. %a)(%a %a)@]@.))@.@."
358
                           (pp_conj (pp_instr true m.mname.node_id)) instrs_concat
359
                           (pp_conj pp_val) assertsl
360
                           pp_machine_init_name m.mname.node_id
361
                           (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m);
362
            (*Rule for step*)
363
            Format.fprintf fmt "@[<v 2>(rule (=> @ (and @ %a@. %a)(%a %a)@]@.))@.@."
364
                           (pp_conj (pp_instr false m.mname.node_id)) instrs_concat
365
                           (pp_conj pp_val) assertsl
366
                           pp_machine_step_name m.mname.node_id
367
                           (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m);
368
          end
369
       );
370
     end
371
    end
372

    
373

    
374

    
375
let collecting_semantics machines fmt node machine =
376
    Format.fprintf fmt "; Collecting semantics for node %s@.@." node;
377
    (* We print the types of the main node "memory tree" TODO: add the output *)
378
    let main_output =
379
     rename_machine_list machine.mname.node_id machine.mstep.step_outputs
380
    in
381
    let main_output_dummy =
382
     rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_outputs
383
    in
384
    let main_memory_next =
385
      (rename_next_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @
386
      main_output
387
    in
388
    let main_memory_current =
389
      (rename_current_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @
390
      main_output_dummy
391
    in
392

    
393
    (* Special case when the main node is stateless *)
394
    let init_name, step_name =
395
      if is_stateless machine then
396
	pp_machine_stateless_name, pp_machine_stateless_name
397
      else
398
	pp_machine_init_name, pp_machine_step_name
399
    in
400

    
401
    Format.fprintf fmt "(declare-rel MAIN (%a))@."
402
      (Utils.fprintf_list ~sep:" " pp_type)
403
      (List.map (fun v -> v.var_type) main_memory_next);
404

    
405
    Format.fprintf fmt "; Initial set@.";
406
    Format.fprintf fmt "(declare-rel INIT_STATE ())@.";
407
    Format.fprintf fmt "(rule INIT_STATE)@.";
408
    Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>INIT_STATE@ (@[<v 0>%a %a@])@]@ )@ (MAIN %a)@]@.))@.@."
409
      init_name node
410
      (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines machine)
411
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_next ;
412

    
413
    Format.fprintf fmt "; Inductive def@.";
414
    (Utils.fprintf_list ~sep:" " (fun fmt v -> Format.fprintf fmt "%a@." pp_decl_var v)) fmt main_output_dummy;
415
    Format.fprintf fmt
416
      "@[<v 2>(rule (=> @ (and @[<v 0>(MAIN %a)@ (@[<v 0>%a %a@])@]@ )@ (MAIN %a)@]@.))@.@."
417
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_current
418
      step_name node
419
      (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines machine)
420
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_next
421

    
422
let check_prop machines fmt node machine =
423
  let main_output =
424
    rename_machine_list machine.mname.node_id machine.mstep.step_outputs
425
  in
426
  let main_memory_next =
427
    (rename_next_list (full_memory_vars machines machine)) @ main_output
428
  in
429
  Format.fprintf fmt "; Property def@.";
430
  Format.fprintf fmt "(declare-rel ERR ())@.";
431
  Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (MAIN %a)@])@ ERR))@."
432
    (pp_conj pp_var) main_output
433
    (Utils.fprintf_list ~sep:" " pp_var) main_memory_next
434
    ;
435
   if !Options.horn_query then Format.fprintf fmt "(query ERR)@."
436

    
437

    
438
let cex_computation machines fmt node machine =
439
    Format.fprintf fmt "; CounterExample computation for node %s@.@." node;
440
    (* We print the types of the cex node "memory tree" TODO: add the output *)
441
    let cex_input =
442
     rename_machine_list machine.mname.node_id machine.mstep.step_inputs
443
    in
444
    let cex_input_dummy =
445
     rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_inputs
446
    in
447
    let cex_output =
448
     rename_machine_list machine.mname.node_id machine.mstep.step_outputs
449
    in
450
    let cex_output_dummy =
451
     rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_outputs
452
    in
453
    let cex_memory_next =
454
      cex_input @ (rename_next_list (full_memory_vars machines machine)) @ cex_output
455
    in
456
    let cex_memory_current =
457
      cex_input_dummy @ (rename_current_list (full_memory_vars machines machine)) @ cex_output_dummy
458
    in
459

    
460
    (* Special case when the cex node is stateless *)
461
    let init_name, step_name =
462
      if is_stateless machine then
463
	pp_machine_stateless_name, pp_machine_stateless_name
464
      else
465
	pp_machine_init_name, pp_machine_step_name
466
    in
467

    
468
    Format.fprintf fmt "(declare-rel CEX (Int %a))@.@."
469
      (Utils.fprintf_list ~sep:" " pp_type)
470
      (List.map (fun v -> v.var_type) cex_memory_next);
471

    
472
    Format.fprintf fmt "; Initial set@.";
473
    Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>INIT_STATE@ (@[<v 0>%a %a@])@]@ )@ (CEX 0 %a)@]@.))@.@."
474
      init_name node
475
      (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines machine)
476
      (Utils.fprintf_list ~sep:" " pp_var) cex_memory_next ;
477

    
478
    Format.fprintf fmt "; Inductive def@.";
479
    (* Declare dummy inputs. Outputs should have been declared previously with collecting sem *)
480
    (Utils.fprintf_list ~sep:" " (fun fmt v -> Format.fprintf fmt "%a@." pp_decl_var v)) fmt cex_input_dummy;
481
    Format.fprintf fmt "(declare-var cexcpt Int)@.";
482
    Format.fprintf fmt
483
      "@[<v 2>(rule (=> @ (and @[<v 0>(CEX cexcpt %a)@ (@[<v 0>%a %a@])@]@ )@ (CEX (+ 1 cexcpt) %a)@]@.))@.@."
484
      (Utils.fprintf_list ~sep:" " pp_var) cex_memory_current
485
      step_name node
486
      (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines machine)
487
      (Utils.fprintf_list ~sep:" " pp_var) cex_memory_next
488

    
489
let get_cex machines fmt node machine =
490
    let cex_input =
491
     rename_machine_list machine.mname.node_id machine.mstep.step_inputs
492
    in
493
    let cex_output =
494
     rename_machine_list machine.mname.node_id machine.mstep.step_outputs
495
    in
496
  let cex_memory_next =
497
    cex_input @ (rename_next_list (full_memory_vars machines machine)) @ cex_output
498
  in
499
  Format.fprintf fmt "; Property def@.";
500
  Format.fprintf fmt "(declare-rel CEXTRACE ())@.";
501
  Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (CEX cexcpt %a)@])@ CEXTRACE))@."
502
    (pp_conj pp_var) cex_output
503
    (Utils.fprintf_list ~sep:" " pp_var) cex_memory_next
504
    ;
505
  Format.fprintf fmt "(query CEXTRACE)@."
506

    
507

    
508
let main_print machines fmt =
509
if !Options.main_node <> "" then
510
  begin
511
    let node = !Options.main_node in
512
    let machine = get_machine machines node in
513

    
514

    
515
    collecting_semantics machines fmt node machine;
516
    check_prop machines fmt node machine;
517
    if !Options.horn_cex then(
518
      cex_computation machines fmt node machine;
519
      get_cex machines fmt node machine)
520
end
521

    
522

    
523
let translate fmt basename prog machines =
524
  List.iter (print_machine machines fmt) (List.rev machines);
525
  main_print machines fmt
526

    
527

    
528
let traces_file fmt basename prog machines =
529

    
530
  Format.fprintf fmt
531
  "<?xml version=\"1.0\"?>\n<Traces xmlns:xsi=\"http://www.w3.org/2001/XMLSchema-instance\">\n";
532

    
533
  (* We extract the annotation dealing with traceability *)
534
  let machines_traces = List.map (fun m ->
535
    let traces : (ident * expr) list=
536
      let all_annots = List.flatten (List.map (fun ann -> ann.annots) m.mannot) in
537
      let filtered =
538
	List.filter (fun (kwds, _) -> kwds = ["traceability"]) all_annots
539
      in
540
      let content = List.map snd filtered in
541
      (* Elements are supposed to be a pair (tuple): variable, expression *)
542
      List.map (fun ee ->
543
	match ee.eexpr_quantifiers, ee.eexpr_qfexpr.expr_desc with
544
	| [], Expr_tuple [v;e] -> (
545
	  match v.expr_desc with
546
	  | Expr_ident vid -> vid, e
547
	  | _ -> assert false )
548
	| _ -> assert false)
549
	content
550
    in
551

    
552
    m, traces
553

    
554
  ) machines
555
  in
556

    
557
  (* Compute memories associated to each machine *)
558
  let compute_mems m =
559
    let rec aux fst prefix m =
560
      (List.map (fun mem -> (prefix, mem)) m.mmemory) @
561
	List.fold_left (fun accu (id, (n, _)) ->
562
	  let name = node_name n in
563
	  if name = "_arrow" then accu else
564
	    let machine_n = get_machine machines name in
565
	    ( aux false ((id,machine_n)::prefix) machine_n )
566
	    @ accu
567
	) [] m.minstances
568
    in
569
    aux true [] m
570
  in
571

    
572
  List.iter (fun m ->
573
    (* Format.fprintf fmt "; Node %s@." m.mname.node_id; *)
574
    Format.fprintf fmt "    <Node name=\"%s\">@." m.mname.node_id;
575

    
576
    let memories_old =
577
      List.map (fun (p, v) ->
578
	let machine = match p with | [] -> m | (_,m')::_ -> m' in
579
	let traces = List.assoc machine machines_traces in
580
	if List.mem_assoc v.var_id traces then (
581
	  (* We take the expression associated to variable v in the trace info *)
582
	  (* Format.eprintf "Found variable %a in traces: %a@."  pp_var v Printers.pp_expr (List.assoc v.var_id traces); *)
583
	  p, List.assoc v.var_id traces
584
      )
585
	else (
586
	  (* We keep the variable as is: we create an expression v *)
587
	  (* Format.eprintf "Unable to found variable %a in traces (%a)@."  pp_var v (Utils.fprintf_list ~sep:", " Format.pp_print_string) (List.map fst traces); *)
588
	  p, mkexpr Location.dummy_loc (Expr_ident v.var_id)
589
	)
590

    
591
      ) (compute_mems m)
592
    in
593
    let memories_next = (* We remove the topest pre in each expression *)
594
      List.map
595
      	(fun (prefix, ee) ->
596
      	  match ee.expr_desc with
597
      	  | Expr_pre e -> prefix, e
598
      	  | _ -> Format.eprintf
599
      	    "Mem Failure: (prefix: %a, eexpr: %a)@.@?"
600
      	    (Utils.fprintf_list ~sep:","
601
      	       (fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id ))
602
      	    (List.rev prefix)
603
      	    Printers.pp_expr ee;
604
      	    assert false)
605
	memories_old
606
    in
607

    
608
    (* let pp_prefix_rev fmt prefix = *)
609
    (*   Utils.fprintf_list ~sep:"." (fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id) fmt (List.rev prefix) *)
610
    (* in *)
611

    
612
    let pp_prefix_rev fmt prefix =
613
      Utils.fprintf_list ~sep:"." (fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id) fmt (List.rev prefix)
614
    in
615

    
616
    let input_vars = (rename_machine_list m.mname.node_id m.mstep.step_inputs) in
617
    let output_vars = (rename_machine_list m.mname.node_id m.mstep.step_outputs) in
618
     Format.fprintf fmt "     <input name=\"%a\" type=\"%a\">%a</input> @."
619
                   (Utils.fprintf_list ~sep:" | " pp_var) input_vars
620
                   (Utils.fprintf_list ~sep:" | "  (fun fmt id -> pp_type fmt id.var_type)) input_vars
621
                   (Utils.fprintf_list ~sep:" | " pp_var) (m.mstep.step_inputs);
622

    
623
    Format.fprintf fmt "      <output name=\"%a\" type=\"%a\">%a</output> @."
624
                   (Utils.fprintf_list ~sep:" | " pp_var)  output_vars
625
                   (Utils.fprintf_list ~sep:" | "  (fun fmt id -> pp_type fmt id.var_type)) output_vars
626
                   (Utils.fprintf_list ~sep:" | " pp_var) (m.mstep.step_outputs);
627

    
628
    let init_local_vars = (rename_next_list (full_memory_vars machines m)) in
629
    let step_local_vars = (rename_current_list (full_memory_vars machines m)) in
630

    
631
    Format.fprintf fmt "      <localInit name=\"%a\" type=\"%a\">%t%a</localInit> @."
632
                   (Utils.fprintf_list ~sep:" | " pp_var) init_local_vars
633
                   (Utils.fprintf_list ~sep:" | "  (fun fmt id -> pp_type fmt id.var_type)) init_local_vars
634
                   (fun fmt -> match memories_next with [] -> () | _ -> fprintf fmt "")
635
                   (Utils.fprintf_list ~sep:" | " (fun fmt (prefix, ee) -> fprintf fmt "%a" Printers.pp_expr ee)) memories_next;
636

    
637
    Format.fprintf fmt "      <localStep name=\"%a\" type=\"%a\">%t%a</localStep> @."
638
                   (Utils.fprintf_list ~sep:" | " pp_var) step_local_vars
639
                   (Utils.fprintf_list ~sep:" | "  (fun fmt id -> pp_type fmt id.var_type)) step_local_vars
640
                   (fun fmt -> match memories_old with [] -> () | _ -> fprintf fmt "")
641
                     (Utils.fprintf_list ~sep:" | " (fun fmt (prefix,ee) -> fprintf fmt "(%a)"
642
                                    Printers.pp_expr ee)) (memories_old);
643

    
644
     Format.fprintf fmt "    </Node>@.";
645

    
646
  ) (List.rev machines);
647
  Format.fprintf fmt "</Traces>@.";
648

    
649
          (* (Utils.fprintf_list ~sep:" | " (fun fmt (prefix, ee) -> fprintf fmt "%a%a" pp_prefix_rev prefix Printers.pp_expr ee)) memories_next; *)
650
   (* (Utils.fprintf_list ~sep:" | " (fun fmt (prefix,ee) -> fprintf fmt "%a(%a)" *)
651
   (*                                  pp_prefix_rev prefix Printers.pp_expr ee)) (memories_old); *)
652

    
653
(* Local Variables: *)
654
(* compile-command:"make -C ../.." *)
655
(* End: *)
    (1-1/1)