Project

General

Profile

Revision 5cf953ec src/backends/Horn/horn_backend.ml

View differences:

src/backends/Horn/horn_backend.ml
32 32
  | Types.Tstatic _
33 33
  | Types.Tconst _
34 34
  | Types.Tarrow _
35
  | _                     -> Format.eprintf "internal error: pp_type %a@." 
35
  | _                     -> Format.eprintf "internal error: pp_type %a@."
36 36
    Types.print_ty t; assert false
37 37

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

  
45 45

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

  
53 52

  
54
let concat prefix x = if prefix = "" then x else prefix ^ "." ^ x 
53

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

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

  
64 64

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

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

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

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

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

  
92 92
(********************************************************************************************)
93 93
(*                    Instruction Printing functions                                        *)
94 94
(********************************************************************************************)
......
121 121
let rec pp_horn_val ?(is_lhs=false) self pp_var fmt v =
122 122
  match v with
123 123
    | Cst c         -> pp_horn_const fmt c
124
    | Array _      
124
    | Array _
125 125
    | Access _ -> assert false (* no arrays *)
126 126
    | Power (v, n)  -> assert false
127 127
    | LocalVar v    -> pp_var fmt (rename_machine self v)
128 128
    | StateVar v    ->
129 129
      if Types.is_array_type v.var_type
130
      then assert false 
130
      then assert false
131 131
      else pp_var fmt (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v))
132 132
    | Fun (n, vl)   -> Format.fprintf fmt "%a" (Basic_library.pp_horn n (pp_horn_val self pp_var)) vl
133 133

  
......
147 147
*)
148 148
let pp_assign m self pp_var fmt var_type var_name value =
149 149
  fprintf fmt "(= %a %a)" (pp_horn_val ~is_lhs:true self pp_var) var_name (pp_value_suffix self pp_var) value
150
  
151
let pp_instance_call 
150

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

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

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

  
......
239 239
    (Utils.fprintf_list ~sep:"@," (pp_machine_instr machines ~init:init  m self)) el
240 240

  
241 241
and pp_machine_instr machines ?(init=false) (m: machine_t) self fmt instr =
242
  match instr with 
242
  match instr with
243 243
  | MReset i ->
244 244
    pp_machine_init m self fmt i
245 245
  | MLocalAssign (i,v) ->
......
250 250
    pp_assign
251 251
      m self (pp_horn_var m) fmt
252 252
      i.var_type (StateVar i) v
253
  | MStep ([i0], i, vl) when Basic_library.is_internal_fun i  -> 
253
  | MStep ([i0], i, vl) when Basic_library.is_internal_fun i  ->
254 254
    assert false (* This should not happen anymore *)
255 255
  | MStep (il, i, vl) ->
256 256
    pp_instance_call machines ~init:init m self fmt i vl il
......
265 265

  
266 266

  
267 267
(**************************************************************)
268
   
269
let is_stateless m = m.minstances = [] && m.mmemory = [] 
270 268

  
271
(* Print the machine m: 
269
let is_stateless m = m.minstances = [] && m.mmemory = []
270

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

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

  
292
   
293
   
292

  
293

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

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

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

  
326 326
       Format.pp_print_newline fmt ();
327 327

  
328 328
       (* Rule for init *)
......
342 342
       | [] -> ()
343 343
       | assertsl -> begin
344 344
	 let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id pp_var in
345
	 
345

  
346 346
	 Format.fprintf fmt "; Asserts@.";
347 347
	 Format.fprintf fmt "(assert @[<v 2>%a@]@ )@.@.@."
348 348
	   (pp_conj pp_val) assertsl;
349
	 
350
	 (** TEME: the following code is the one we described. But it generates a segfault in z3 
349

  
350
	 (** TEME: the following code is the one we described. But it generates a segfault in z3
351 351
	 Format.fprintf fmt "; Asserts for init@.";
352 352
	 Format.fprintf fmt "@[<v 2>(assert (=> @ (and @[<v 0>%a@]@ (%a %a))@ %a@]@.))@.@.@."
353 353
	   (Utils.fprintf_list ~sep:"@ " (pp_instr true m.mname.node_id)) m.mstep.step_instrs
354 354
	   pp_machine_init_name m.mname.node_id
355 355
	   (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m)
356
	   (pp_conj pp_val) assertsl; 
357
	  
356
	   (pp_conj pp_val) assertsl;
357

  
358 358
	 Format.fprintf fmt "; Asserts for step@.";
359 359
	 Format.fprintf fmt "@[<v 2>(assert (=> @ (and @[<v 0>%a@]@ (%a %a))@ %a@]@.))@.@."
360 360
	   (Utils.fprintf_list ~sep:"@ " (pp_instr false m.mname.node_id)) m.mstep.step_instrs
......
365 365
      	 *)
366 366
       end
367 367
       );
368
       
368

  
369 369
(*
370 370
       match m.mspec with
371 371
	 None -> () (* No node spec; we do nothing *)
372
       | Some {requires = []; ensures = [EnsuresExpr e]; behaviors = []} -> 
373
	 ( 
372
       | Some {requires = []; ensures = [EnsuresExpr e]; behaviors = []} ->
373
	 (
374 374
       (* For the moment, we only deal with simple case: single ensures, no other parameters *)
375 375
	   ()
376
	     
376

  
377 377
	 )
378 378
       | _ -> () (* Other cases give nothing *)
379
*)      
379
*)
380 380
     end
381 381
    end
382 382

  
......
388 388
    let main_output =
389 389
     rename_machine_list machine.mname.node_id machine.mstep.step_outputs
390 390
    in
391
    let main_output_dummy = 
391
    let main_output_dummy =
392 392
     rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_outputs
393 393
    in
394
    let main_memory_next = 
394
    let main_memory_next =
395 395
      (rename_next_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @
396 396
      main_output
397 397
    in
398
    let main_memory_current = 
398
    let main_memory_current =
399 399
      (rename_current_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @
400 400
      main_output_dummy
401 401
    in
402 402

  
403 403
    (* Special case when the main node is stateless *)
404
    let init_name, step_name = 
404
    let init_name, step_name =
405 405
      if is_stateless machine then
406 406
	pp_machine_stateless_name, pp_machine_stateless_name
407 407
      else
......
409 409
    in
410 410

  
411 411
    Format.fprintf fmt "(declare-rel MAIN (%a))@."
412
      (Utils.fprintf_list ~sep:" " pp_type) 
412
      (Utils.fprintf_list ~sep:" " pp_type)
413 413
      (List.map (fun v -> v.var_type) main_memory_next);
414
    
414

  
415 415
    Format.fprintf fmt "; Initial set@.";
416 416
    Format.fprintf fmt "(declare-rel INIT_STATE ())@.";
417 417
    Format.fprintf fmt "(rule INIT_STATE)@.";
......
422 422

  
423 423
    Format.fprintf fmt "; Inductive def@.";
424 424
    (Utils.fprintf_list ~sep:" " (fun fmt v -> Format.fprintf fmt "%a@." pp_decl_var v)) fmt main_output_dummy;
425
    Format.fprintf fmt 
425
    Format.fprintf fmt
426 426
      "@[<v 2>(rule (=> @ (and @[<v 0>(MAIN %a)@ (@[<v 0>%a %a@])@]@ )@ (MAIN %a)@]@.))@.@."
427 427
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_current
428 428
      step_name node
429 429
      (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines machine)
430
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_next 
430
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_next
431 431

  
432 432
let check_prop machines fmt node machine =
433 433
  let main_output =
434 434
    rename_machine_list machine.mname.node_id machine.mstep.step_outputs
435 435
  in
436
  let main_memory_next = 
436
  let main_memory_next =
437 437
    (rename_next_list (full_memory_vars machines machine)) @ main_output
438 438
  in
439 439
  Format.fprintf fmt "; Property def@.";
......
452 452
    let cex_input =
453 453
     rename_machine_list machine.mname.node_id machine.mstep.step_inputs
454 454
    in
455
    let cex_input_dummy = 
455
    let cex_input_dummy =
456 456
     rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_inputs
457 457
    in
458 458
    let cex_output =
459 459
     rename_machine_list machine.mname.node_id machine.mstep.step_outputs
460 460
    in
461
    let cex_output_dummy = 
461
    let cex_output_dummy =
462 462
     rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_outputs
463 463
    in
464
    let cex_memory_next = 
464
    let cex_memory_next =
465 465
      cex_input @ (rename_next_list (full_memory_vars machines machine)) @ cex_output
466 466
    in
467
    let cex_memory_current = 
467
    let cex_memory_current =
468 468
      cex_input_dummy @ (rename_current_list (full_memory_vars machines machine)) @ cex_output_dummy
469 469
    in
470 470

  
471 471
    (* Special case when the cex node is stateless *)
472
    let init_name, step_name = 
472
    let init_name, step_name =
473 473
      if is_stateless machine then
474 474
	pp_machine_stateless_name, pp_machine_stateless_name
475 475
      else
......
477 477
    in
478 478

  
479 479
    Format.fprintf fmt "(declare-rel CEX (Int %a))@.@."
480
      (Utils.fprintf_list ~sep:" " pp_type) 
480
      (Utils.fprintf_list ~sep:" " pp_type)
481 481
      (List.map (fun v -> v.var_type) cex_memory_next);
482
    
482

  
483 483
    Format.fprintf fmt "; Initial set@.";
484 484
    Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>INIT_STATE@ (@[<v 0>%a %a@])@]@ )@ (CEX 0 %a)@]@.))@.@."
485 485
      init_name node
......
490 490
    (* Declare dummy inputs. Outputs should have been declared previously with collecting sem *)
491 491
    (Utils.fprintf_list ~sep:" " (fun fmt v -> Format.fprintf fmt "%a@." pp_decl_var v)) fmt cex_input_dummy;
492 492
    Format.fprintf fmt "(declare-var cexcpt Int)@.";
493
    Format.fprintf fmt 
493
    Format.fprintf fmt
494 494
      "@[<v 2>(rule (=> @ (and @[<v 0>(CEX cexcpt %a)@ (@[<v 0>%a %a@])@]@ )@ (CEX (+ 1 cexcpt) %a)@]@.))@.@."
495 495
      (Utils.fprintf_list ~sep:" " pp_var) cex_memory_current
496 496
      step_name node
497 497
      (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines machine)
498
      (Utils.fprintf_list ~sep:" " pp_var) cex_memory_next 
498
      (Utils.fprintf_list ~sep:" " pp_var) cex_memory_next
499 499

  
500 500
let get_cex machines fmt node machine =
501 501
    let cex_input =
......
504 504
    let cex_output =
505 505
     rename_machine_list machine.mname.node_id machine.mstep.step_outputs
506 506
    in
507
  let cex_memory_next = 
507
  let cex_memory_next =
508 508
    cex_input @ (rename_next_list (full_memory_vars machines machine)) @ cex_output
509 509
  in
510 510
  Format.fprintf fmt "; Property def@.";
......
517 517
    Format.fprintf fmt "(query CEXTRACE)@."
518 518

  
519 519

  
520
let main_print machines fmt = 
521
if !Options.main_node <> "" then 
520
let main_print machines fmt =
521
if !Options.main_node <> "" then
522 522
  begin
523 523
    let node = !Options.main_node in
524 524
    let machine = get_machine machines node in
......
534 534

  
535 535
let translate fmt basename prog machines =
536 536
  List.iter (print_machine machines fmt) (List.rev machines);
537
  
538
  main_print machines fmt 
537

  
538
  main_print machines fmt
539 539

  
540 540

  
541 541
let traces_file fmt basename prog machines =
542
  Format.fprintf fmt 
542
  Format.fprintf fmt
543 543
    "; Horn code traceability generated by %s@.; SVN version number %s@.@."
544
    (Filename.basename Sys.executable_name) 
544
    (Filename.basename Sys.executable_name)
545 545
    Version.number;
546 546

  
547 547
  (* We extract the annotation dealing with traceability *)
548
  let machines_traces = List.map (fun m -> 
549
    let traces : (ident * expr) list= 
548
  let machines_traces = List.map (fun m ->
549
    let traces : (ident * expr) list=
550 550
      let all_annots = List.flatten (List.map (fun ann -> ann.annots) m.mannot) in
551
      let filtered = 
552
	List.filter (fun (kwds, _) -> kwds = ["horn_backend";"trace"]) all_annots 
551
      let filtered =
552
	List.filter (fun (kwds, _) -> kwds = ["horn_backend";"trace"]) all_annots
553 553
      in
554 554
      let content = List.map snd filtered in
555 555
      (* Elements are supposed to be a pair (tuple): variable, expression *)
556
      List.map (fun ee -> 
557
	match ee.eexpr_quantifiers, ee.eexpr_qfexpr.expr_desc with 
556
      List.map (fun ee ->
557
	match ee.eexpr_quantifiers, ee.eexpr_qfexpr.expr_desc with
558 558
	| [], Expr_tuple [v;e] -> (
559
	  match v.expr_desc with 
560
	  | Expr_ident vid -> vid, e 
559
	  match v.expr_desc with
560
	  | Expr_ident vid -> vid, e
561 561
	  | _ -> assert false )
562 562
	| _ -> assert false)
563 563
	content
564 564
    in
565
    
565

  
566 566
    m, traces
567 567

  
568 568
  ) machines
......
572 572
  let compute_mems m =
573 573
    let rec aux fst prefix m =
574 574
      (List.map (fun mem -> (prefix, mem)) m.mmemory) @
575
	List.fold_left (fun accu (id, (n, _)) -> 
576
	  let name = node_name n in 
575
	List.fold_left (fun accu (id, (n, _)) ->
576
	  let name = node_name n in
577 577
	  if name = "_arrow" then accu else
578 578
	    let machine_n = get_machine machines name in
579
	    ( aux false ((id,machine_n)::prefix) machine_n ) 
579
	    ( aux false ((id,machine_n)::prefix) machine_n )
580 580
	    @ accu
581
	) [] m.minstances 
581
	) [] m.minstances
582 582
    in
583 583
    aux true [] m
584 584
  in
585 585

  
586 586
  List.iter (fun m ->
587 587
    Format.fprintf fmt "; Node %s@." m.mname.node_id;
588
    
589
    let memories_old = 
590
      List.map (fun (p, v) -> 
588

  
589
    let memories_old =
590
      List.map (fun (p, v) ->
591 591
	let machine = match p with | [] -> m | (_,m')::_ -> m' in
592 592
	let traces = List.assoc machine machines_traces in
593 593
	if List.mem_assoc v.var_id traces then
......
596 596
	else
597 597
	  (* We keep the variable as is: we create an expression v *)
598 598
	  p, mkexpr Location.dummy_loc (Expr_ident v.var_id)
599
	    
600
      ) (compute_mems m) 
599

  
600
      ) (compute_mems m)
601 601
    in
602 602
    let memories_next = (* We remove the topest pre in each expression *)
603
      List.map 
604
	(fun (prefix, ee) -> 
605
	  match ee.expr_desc with 
606
	  | Expr_pre e -> prefix, e 
607
	  | _ -> Format.eprintf 
608
	    "Mem Failure: (prefix: %a, eexpr: %a)@.@?" 
609
	    (Utils.fprintf_list ~sep:"," 
610
	       (fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id )) 
611
	    (List.rev prefix) 
612
	    Printers.pp_expr ee; 
603
      List.map
604
	(fun (prefix, ee) ->
605
	  match ee.expr_desc with
606
	  | Expr_pre e -> prefix, e
607
	  | _ -> Format.eprintf
608
	    "Mem Failure: (prefix: %a, eexpr: %a)@.@?"
609
	    (Utils.fprintf_list ~sep:","
610
	       (fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id ))
611
	    (List.rev prefix)
612
	    Printers.pp_expr ee;
613 613
	    assert false)
614 614
	memories_old
615 615
    in
......
645 645
      (Utils.fprintf_list ~sep:" " pp_var) (m.mstep.step_inputs@m.mstep.step_outputs)
646 646
      (fun fmt -> match memories_old with [] -> () | _ -> fprintf fmt " ")
647 647
      (Utils.fprintf_list ~sep:" " (fun fmt (prefix,ee) -> fprintf fmt "%a(%a)" pp_prefix_rev prefix Printers.pp_expr ee)) (memories_old@memories_next);
648
    Format.pp_print_newline fmt ();    
648
    Format.pp_print_newline fmt ();
649 649
  ) (List.rev machines);
650
  
650

  
651 651

  
652 652
(* Local Variables: *)
653 653
(* compile-command:"make -C .." *)

Also available in: Unified diff