Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / horn_backend.ml @ af5af1e8

History | View | Annotate | Download (22.8 KB)

1
open Format
2
open LustreSpec
3
open Corelang
4
open Machine_code
5

    
6

    
7
let pp_machine_init_name fmt id = fprintf fmt "%s_init" id
8
let pp_machine_step_name fmt id = fprintf fmt "%s_step" id
9
let pp_machine_stateless_name fmt id = fprintf fmt "%s" id
10

    
11
let pp_type fmt t =
12
  match (Types.repr t).Types.tdesc with
13
  | Types.Tbool           -> Format.fprintf fmt "Bool"
14
  | Types.Tint            -> Format.fprintf fmt "Int"
15
  | Types.Treal           -> Format.fprintf fmt "Real"
16
  | Types.Tclock _
17
  | Types.Tarray _
18
  | Types.Tstatic _
19
  | Types.Tconst _
20
  | Types.Tarrow _
21
  | _                     -> Format.eprintf "internal error: pp_type %a@." 
22
                             Types.print_ty t; assert false
23

    
24
let pp_decl_var fmt id = 
25
  Format.fprintf fmt "(declare-var %s %a)"
26
    id.var_id
27
    pp_type id.var_type
28

    
29
let pp_var fmt id = Format.pp_print_string fmt id.var_id
30

    
31

    
32
let pp_conj pp fmt l = 
33
  match l with 
34
    [] -> assert false
35
  | [x] -> pp fmt x
36
  | _ -> fprintf fmt "(and @[<v 0>%a@]@ )" (Utils.fprintf_list ~sep:" " pp) l
37
    
38

    
39

    
40
let concat prefix x = if prefix = "" then x else prefix ^ "." ^ x 
41
let rename f = (fun v -> {v with var_id = f v.var_id } )
42
let rename_machine p = rename (fun n -> concat p n)
43
let rename_machine_list p = List.map (rename_machine p)
44
    
45
let rename_current =  rename (fun n -> n ^ "_c")
46
let rename_current_list = List.map rename_current
47
let rename_next = rename (fun n -> n ^ "_x")
48
let rename_next_list = List.map rename_next
49

    
50

    
51
let get_machine machines node_name = 
52
  List.find (fun m  -> m.mname.node_id = node_name) machines 
53

    
54
let full_memory_vars machines machine =
55
  let rec aux fst prefix m =
56
    (rename_machine_list (if fst then prefix else concat prefix m.mname.node_id) m.mmemory) @
57
      List.fold_left (fun accu (id, (n, _)) -> 
58
	let name = node_name n in 
59
	if name = "_arrow" then accu else
60
	  let machine_n = get_machine machines name in
61
	( aux false (concat prefix (if fst then id else concat m.mname.node_id id)) machine_n ) @ accu
62
      ) [] (m.minstances) 
63
  in
64
  aux true machine.mname.node_id machine
65

    
66
let stateless_vars machines m = 
67
  (rename_machine_list m.mname.node_id m.mstep.step_inputs)@
68
    (rename_machine_list m.mname.node_id m.mstep.step_outputs)
69
    
70
let step_vars machines m = 
71
  (stateless_vars machines m)@
72
    (rename_current_list (full_memory_vars machines m)) @ 
73
    (rename_next_list (full_memory_vars machines m)) 
74
    
75
let init_vars machines m = 
76
  (stateless_vars machines m) @ (rename_next_list (full_memory_vars machines m)) 
77
    
78
(********************************************************************************************)
79
(*                    Instruction Printing functions                                        *)
80
(********************************************************************************************)
81

    
82
let pp_horn_var m fmt id =
83
  if Types.is_array_type id.var_type
84
  then
85
    assert false (* no arrays in Horn output *)
86
  else
87
    Format.fprintf fmt "%s" id.var_id
88

    
89

    
90
(* Used to print boolean constants *)
91
let pp_horn_tag fmt t =
92
  pp_print_string fmt (if t = tag_true then "true" else if t = tag_false then "false" else t)
93

    
94
(* Prints a constant value *)
95
let rec pp_horn_const fmt c =
96
  match c with
97
    | Const_int i    -> pp_print_int fmt i
98
    | Const_real r   -> pp_print_string fmt r
99
    | Const_float r  -> pp_print_float fmt r
100
    | Const_tag t    -> pp_horn_tag fmt t
101
    | _              -> assert false
102

    
103
(* Prints a value expression [v], with internal function calls only.
104
   [pp_var] is a printer for variables (typically [pp_c_var_read]),
105
   but an offset suffix may be added for array variables
106
*)
107
let rec pp_horn_val ?(is_lhs=false) self pp_var fmt v =
108
  match v with
109
    | Cst c         -> pp_horn_const fmt c
110
    | Array _      
111
    | Access _ -> assert false (* no arrays *)
112
    | Power (v, n)  -> assert false
113
    | LocalVar v    -> pp_var fmt (rename_machine self v)
114
    | StateVar v    ->
115
      if Types.is_array_type v.var_type
116
      then assert false 
117
      else pp_var fmt (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v))
118
    | Fun (n, vl)   -> Format.fprintf fmt "%a" (Basic_library.pp_horn n (pp_horn_val self pp_var)) vl
119

    
120
(* Prints a [value] indexed by the suffix list [loop_vars] *)
121
let rec pp_value_suffix self pp_value fmt value =
122
 match value with
123
 | Fun (n, vl)  ->
124
   Basic_library.pp_horn n (pp_value_suffix self pp_value) fmt vl
125
 |  _            ->
126
   pp_horn_val self pp_value fmt value
127

    
128
(* type_directed assignment: array vs. statically sized type
129
   - [var_type]: type of variable to be assigned
130
   - [var_name]: name of variable to be assigned
131
   - [value]: assigned value
132
   - [pp_var]: printer for variables
133
*)
134
let pp_assign m self pp_var fmt var_type var_name value =
135
  fprintf fmt "(= %a %a)" (pp_horn_val ~is_lhs:true self pp_var) var_name (pp_value_suffix self pp_var) value
136
  
137
let pp_instance_call 
138
    machines ?(init=false) m self fmt i (inputs: value_t list) (outputs: var_decl list) =
139
  try (* stateful node instance *) 
140
    begin
141
      let (n,_) = List.assoc i m.minstances in
142
      match node_name n, inputs, outputs with
143
      | "_arrow", [i1; i2], [o] -> begin
144
        if init then
145
          pp_assign
146
   	    m
147
   	    self
148
   	    (pp_horn_var m) 
149
	    fmt
150
   	    o.var_type (LocalVar o) i1
151
        else
152
          pp_assign
153
   	    m self (pp_horn_var m) fmt
154
   	    o.var_type (LocalVar o) i2
155
	    
156
      end
157
      | name, _, _ ->  
158
	begin
159
	  let target_machine = List.find (fun m  -> m.mname.node_id = name) machines in
160
	  if init then
161
	    Format.fprintf fmt "(%a %a%t%a%t%a)"
162
	      pp_machine_init_name (node_name n) 
163
	      (* inputs *)
164
	      (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) 
165
	      inputs
166
	      (Utils.pp_final_char_if_non_empty " " inputs) 
167
	      (* outputs *)
168
	      (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) 
169
	      (List.map (fun v -> LocalVar v) outputs)
170
	      (Utils.pp_final_char_if_non_empty " " outputs)
171
	      (* memories (next) *)
172
	      (Utils.fprintf_list ~sep:" " pp_var) (
173
  		rename_machine_list 
174
		  (concat m.mname.node_id i) 
175
		  (rename_next_list (full_memory_vars machines target_machine)
176
		  ) 
177
	       )
178
	  else
179
	    Format.fprintf fmt "(%a %a%t%a%t%a)"
180
	      pp_machine_step_name (node_name n) 
181
	      (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) inputs
182
	      (Utils.pp_final_char_if_non_empty " " inputs) 
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
	      (Utils.fprintf_list ~sep:" " pp_var) (
187
		(rename_machine_list 
188
		   (concat m.mname.node_id i) 
189
		   (rename_current_list (full_memory_vars machines target_machine))
190
		) @ 
191
		  (rename_machine_list 
192
		     (concat m.mname.node_id i) 
193
		     (rename_next_list (full_memory_vars machines target_machine))
194
		  ) 
195
	       )
196
	    
197
	end
198
    end
199
    with Not_found -> ( (* stateless node instance *)
200
      let (n,_) = List.assoc i m.mcalls in
201
      Format.fprintf fmt "(%s %a%t%a)"
202
	(node_name n)
203
	(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) 
204
	inputs
205
	(Utils.pp_final_char_if_non_empty " " inputs) 
206
	(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) 
207
	(List.map (fun v -> LocalVar v) outputs)
208
    )
209

    
210
let pp_machine_init (m: machine_t) self fmt inst =
211
  let (node, static) = List.assoc inst m.minstances in
212
  fprintf fmt "(%a %a%t%s->%s)"
213
    pp_machine_init_name (node_name node)
214
    (Utils.fprintf_list ~sep:" " Dimension.pp_dimension) static
215
    (Utils.pp_final_char_if_non_empty " " static)
216
    self inst
217

    
218
(* TODO *)
219
let rec pp_conditional machines ?(init=false)  (m: machine_t) self fmt c tl el =
220
  fprintf fmt "@[<v 2>if (%a) {%t%a@]@,@[<v 2>} else {%t%a@]@,}"
221
    (pp_horn_val self (pp_horn_var m)) c
222
    (Utils.pp_newline_if_non_empty tl)
223
    (Utils.fprintf_list ~sep:"@," (pp_machine_instr machines ~init:init  m self)) tl
224
    (Utils.pp_newline_if_non_empty el)
225
    (Utils.fprintf_list ~sep:"@," (pp_machine_instr machines ~init:init  m self)) el
226

    
227
and pp_machine_instr machines ?(init=false) (m: machine_t) self fmt instr =
228
  match instr with 
229
  | MReset i ->
230
    pp_machine_init m self fmt i
231
  | MLocalAssign (i,v) ->
232
    pp_assign
233
      m self (pp_horn_var m) fmt
234
      i.var_type (LocalVar i) v
235
  | MStateAssign (i,v) ->
236
    pp_assign
237
      m self (pp_horn_var m) fmt
238
      i.var_type (StateVar i) v
239
  | MStep ([i0], i, vl) when Basic_library.is_internal_fun i  -> 
240
    assert false (* This should not happen anymore *)
241
  | MStep (il, i, vl) ->
242
    pp_instance_call machines ~init:init m self fmt i vl il
243
  | MBranch (g,hl) ->
244
    if hl <> [] && let t = fst (List.hd hl) in t = tag_true || t = tag_false
245
    then (* boolean case, needs special treatment in C because truth value is not unique *)
246
      (* may disappear if we optimize code by replacing last branch test with default *)
247
      let tl = try List.assoc tag_true  hl with Not_found -> [] in
248
      let el = try List.assoc tag_false hl with Not_found -> [] in
249
      pp_conditional machines ~init:init m self fmt g tl el
250
    else assert false (* enum type case *)
251

    
252

    
253
(**************************************************************)
254
   
255
let is_stateless m = m.minstances = [] && m.mmemory = [] 
256

    
257
(* Print the machine m: 
258
   two functions: m_init and m_step
259
   - m_init is a predicate over m memories
260
   - m_step is a predicate over old_memories, inputs, new_memories, outputs
261
   We first declare all variables then the two /rules/.
262
*)
263
let print_machine machines fmt m = 
264
  let pp_instr init = pp_machine_instr machines ~init:init m in
265
  if m.mname.node_id = arrow_id then 
266
    (* We don't print arrow function *)
267
    ()
268
  else 
269
    begin 
270
      Format.fprintf fmt "; %s@." m.mname.node_id;
271

    
272
   (* Printing variables *)
273
   Utils.fprintf_list ~sep:"@." pp_decl_var fmt 
274
     ((step_vars machines m)@
275
	 (rename_machine_list m.mname.node_id m.mstep.step_locals));
276
   Format.pp_print_newline fmt ();
277

    
278
   
279
   
280
   if is_stateless m then
281
     begin
282
       (* Declaring single predicate *)
283
       Format.fprintf fmt "(declare-rel %a (%a))@."
284
	 pp_machine_stateless_name m.mname.node_id
285
	 (Utils.fprintf_list ~sep:" " pp_type) 
286
	 (List.map (fun v -> v.var_type) (stateless_vars machines m));
287
       
288
       (* Rule for single predicate *)
289
       Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@."
290
	 (pp_conj (pp_instr 
291
		     true (* In this case, the boolean init can be set to true or false. 
292
			     The node is stateless. *)
293
		     m.mname.node_id)
294
	 )
295
	 m.mstep.step_instrs
296
	 pp_machine_stateless_name m.mname.node_id
297
	 (Utils.fprintf_list ~sep:" " pp_var) (stateless_vars machines m);
298
     end
299
   else 
300
     begin
301
       (* Declaring predicate *)
302
       Format.fprintf fmt "(declare-rel %a (%a))@."
303
	 pp_machine_init_name m.mname.node_id
304
	 (Utils.fprintf_list ~sep:" " pp_type) 
305
	 (List.map (fun v -> v.var_type) (init_vars machines m));
306
       
307
       Format.fprintf fmt "(declare-rel %a (%a))@."
308
	 pp_machine_step_name m.mname.node_id
309
	 (Utils.fprintf_list ~sep:" " pp_type) 
310
	 (List.map (fun v -> v.var_type) (step_vars machines m));
311
       
312
       Format.pp_print_newline fmt ();
313

    
314
       (* Rule for init *)
315
       Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@."
316
	 (pp_conj (pp_instr true m.mname.node_id)) m.mstep.step_instrs
317
	 pp_machine_init_name m.mname.node_id
318
	 (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m);
319

    
320
       (* Rule for step *)
321
       Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@."
322
	 (pp_conj (pp_instr false m.mname.node_id)) m.mstep.step_instrs
323
	 pp_machine_step_name m.mname.node_id
324
	 (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m);
325

    
326
       (* Adding assertions *)
327
       (match m.mstep.step_asserts with
328
       | [] -> ()
329
       | assertsl -> begin
330
	 let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id pp_var in
331
	 
332
	 Format.fprintf fmt "; Asserts@.";
333
	 Format.fprintf fmt "(assert @[<v 2>%a@]@ )@.@.@."
334
	   (pp_conj pp_val) assertsl;
335
	 
336
	 (** TEME: the following code is the one we described. But it generates a segfault in z3 
337
	 Format.fprintf fmt "; Asserts for init@.";
338
	 Format.fprintf fmt "@[<v 2>(assert (=> @ (and @[<v 0>%a@]@ (%a %a))@ %a@]@.))@.@.@."
339
	   (Utils.fprintf_list ~sep:"@ " (pp_instr true m.mname.node_id)) m.mstep.step_instrs
340
	   pp_machine_init_name m.mname.node_id
341
	   (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m)
342
	   (pp_conj pp_val) assertsl; 
343
	  
344
	 Format.fprintf fmt "; Asserts for step@.";
345
	 Format.fprintf fmt "@[<v 2>(assert (=> @ (and @[<v 0>%a@]@ (%a %a))@ %a@]@.))@.@."
346
	   (Utils.fprintf_list ~sep:"@ " (pp_instr false m.mname.node_id)) m.mstep.step_instrs
347

    
348
	   pp_machine_step_name m.mname.node_id
349
	   (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m)
350
	   (pp_conj pp_val) assertsl
351
      	 *)
352
       end
353
       );
354
       
355
(*
356
       match m.mspec with
357
	 None -> () (* No node spec; we do nothing *)
358
       | Some {requires = []; ensures = [EnsuresExpr e]; behaviors = []} -> 
359
	 ( 
360
       (* For the moment, we only deal with simple case: single ensures, no other parameters *)
361
	   ()
362
	     
363
	 )
364
       | _ -> () (* Other cases give nothing *)
365
*)      
366
     end
367
    end
368

    
369

    
370

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

    
389
    (* Special case when the main node is stateless *)
390
    let init_name, step_name = 
391
      if is_stateless machine then
392
	pp_machine_stateless_name, pp_machine_stateless_name
393
      else
394
	pp_machine_init_name, pp_machine_step_name
395
    in
396

    
397
    Format.fprintf fmt "(declare-rel MAIN (%a))@."
398
      (Utils.fprintf_list ~sep:" " pp_type) 
399
      (List.map (fun v -> v.var_type) main_memory_next);
400
    
401
    Format.fprintf fmt "; Initial set@.";
402
    Format.fprintf fmt "(declare-rel INIT_STATE ())@.";
403
    Format.fprintf fmt "(rule INIT_STATE)@.";
404
    Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>INIT_STATE@ (@[<v 0>%a %a@])@]@ )@ (MAIN %a)@]@.))@.@."
405
      init_name node
406
      (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines machine)
407
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_next ;
408

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

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

    
434

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

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

    
465
    Format.fprintf fmt "(declare-rel CEX (Int %a))@.@."
466
      (Utils.fprintf_list ~sep:" " pp_type) 
467
      (List.map (fun v -> v.var_type) cex_memory_next);
468
    
469
    Format.fprintf fmt "; Initial set@.";
470
    Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>INIT_STATE@ (@[<v 0>%a %a@])@]@ )@ (CEX 0 %a)@]@.))@.@."
471
      init_name node
472
      (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines machine)
473
      (Utils.fprintf_list ~sep:" " pp_var) cex_memory_next ;
474

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

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

    
505

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

    
512

    
513
    collecting_semantics machines fmt node machine;
514
    check_prop machines fmt node machine;
515

    
516
    cex_computation machines fmt node machine;
517
    get_cex machines fmt node machine 
518
end
519

    
520

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

    
526

    
527
let traces_file fmt basename prog machines =
528
  Format.fprintf fmt 
529
    "; Horn code traceability generated by %s@.; SVN version number %s@.@."
530
    (Filename.basename Sys.executable_name) 
531
    Version.number;
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 = ["horn_backend";"trace"]) 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
    
575
    let memories_old = 
576
      List.map (fun (p, v) -> 
577
	let machine = match p with | [] -> m | (_,m')::_ -> m' in
578
	let traces = List.assoc machine machines_traces in
579
	if List.mem_assoc v.var_id traces then
580
	  (* We take the expression associated to variable v in the trace info *)
581
	  p, List.assoc v.var_id traces
582
	else
583
	  (* We keep the variable as is: we create an expression v *)
584
	  p, mkexpr Location.dummy_loc (Expr_ident v.var_id)
585
	    
586
      ) (compute_mems m) 
587
    in
588
    let memories_next = (* We remove the topest pre in each expression *)
589
      List.map 
590
	(fun (prefix, ee) -> 
591
	  match ee.expr_desc with 
592
	  | Expr_pre e -> prefix, e 
593
	  | _ -> Format.eprintf 
594
	    "Mem Failure: (prefix: %a, eexpr: %a)@.@?" 
595
	    (Utils.fprintf_list ~sep:"," 
596
	       (fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id )) 
597
	    (List.rev prefix) 
598
	    Printers.pp_expr ee; 
599
	    assert false)
600
	memories_old
601
    in
602

    
603
    let pp_prefix_rev fmt prefix =
604
      Utils.fprintf_list ~sep:"." (fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id) fmt (List.rev prefix)
605
    in
606

    
607
    Format.fprintf fmt "; Init predicate@.";
608

    
609
    Format.fprintf fmt "; horn encoding@.";
610
    Format.fprintf fmt "(%a %a)@."
611
      pp_machine_init_name m.mname.node_id
612
      (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m);
613

    
614
    Format.fprintf fmt "; original expressions@.";
615
    Format.fprintf fmt "(%a %a%t%a)@."
616
      pp_machine_init_name m.mname.node_id
617
      (Utils.fprintf_list ~sep:" " pp_var) (m.mstep.step_inputs@m.mstep.step_outputs)
618
      (fun fmt -> match memories_next with [] -> () | _ -> fprintf fmt " ")
619
      (Utils.fprintf_list ~sep:" " (fun fmt (prefix, ee) -> fprintf fmt "%a(%a)" pp_prefix_rev prefix Printers.pp_expr ee)) memories_next;
620

    
621
    Format.pp_print_newline fmt ();
622
    Format.fprintf fmt "; Step predicate@.";
623

    
624
    Format.fprintf fmt "; horn encoding@.";
625
    Format.fprintf fmt "(%a %a)@."
626
      pp_machine_step_name m.mname.node_id
627
      (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m);
628
    Format.fprintf fmt "; original expressions@.";
629
    Format.fprintf fmt "(%a %a%t%a)@."
630
      pp_machine_step_name m.mname.node_id
631
      (Utils.fprintf_list ~sep:" " pp_var) (m.mstep.step_inputs@m.mstep.step_outputs)
632
      (fun fmt -> match memories_old with [] -> () | _ -> fprintf fmt " ")
633
      (Utils.fprintf_list ~sep:" " (fun fmt (prefix,ee) -> fprintf fmt "%a(%a)" pp_prefix_rev prefix Printers.pp_expr ee)) (memories_old@memories_next);
634
    Format.pp_print_newline fmt ();    
635
  ) (List.rev machines);
636
  
637

    
638
(* Local Variables: *)
639
(* compile-command:"make -C .." *)
640
(* End: *)