Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / backends / Horn / horn_backend.ml @ 5500edb8

History | View | Annotate | Download (29 KB)

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

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

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

    
20

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

    
25
let empty_array_var m dim = m.mname.node_id  ^ "_empty_array_" ^ string_of_int dim
26

    
27
(* Common function to build array both for expressions and constants *)
28
let build_array_string element_builder empty_array_var_name vl =
29
  match vl with 
30
  | [] -> assert false 
31
  | vl_hd::vl_tl ->
32
    begin
33
      (* Array assigned. We declare it as var = (store  (store var 1 e1) 2 e2) *)
34
      let rec build_array element_builder list idx accu = 
35
	match list with
36
	| [] -> accu
37
	| hd::tl -> (
38
	  fprintf str_formatter "(store %s %i %a)"
39
	    accu
40
	    idx
41
	    element_builder hd;
42
	  build_array element_builder tl (idx+1) (flush_str_formatter ())
43
	)
44
      in
45
      build_array element_builder
46
	vl_tl 
47
	2 
48
	( (* store 1 vl_hd var_name *)
49
	  fprintf str_formatter "(store %s 1 %a)"
50
	    empty_array_var_name
51
	    element_builder vl_hd;
52
	  flush_str_formatter ()
53
	)
54
    end
55

    
56

    
57
let pp_horn_basic_type fmt t =
58
  match (Types.repr t).Types.tdesc with
59
  | Types.Tbool           -> fprintf fmt "Bool"
60
  | Types.Tint            -> fprintf fmt "Int"
61
  | Types.Treal           -> fprintf fmt "Real"
62
  | _ -> assert false (* Not a basic type *)
63

    
64
let rec pp_horn_type fmt t =
65
  match (Types.repr t).Types.tdesc with
66
  | Types.Tclock t' -> pp_horn_type fmt t' 
67
  | Types.Tbool  | Types.Tint | Types.Treal -> pp_horn_basic_type fmt t
68
  | Types.Tarray (_, t') ->     (* Arrays should be indexed by int *)
69
    fprintf fmt "(Array Int %a)" pp_horn_type t'
70
  | Types.Tstatic (_, t') -> (* Static types are declared as regular types *)
71
    pp_horn_type fmt t'
72
  | Types.Tconst _ (* ty -> fprintf fmt "%s %s" ty var -- from C backend *)
73
  | _ (* (Trat|Tarrow (_, _)|Ttuple _|Tenum _|Tstruct _|Tlink _|Tvar|Tunivar) *)
74
    -> Format.eprintf "internal error: pp_type const %a@." Types.print_ty t; assert false
75
      
76
let pp_decl_var fmt id =
77
  Format.fprintf fmt "(declare-var %s %a)"
78
    id.var_id
79
    pp_horn_type id.var_type
80

    
81
let pp_var fmt id = Format.pp_print_string fmt id.var_id
82

    
83

    
84
let pp_conj pp fmt l =
85
  match l with
86
    [] -> assert false
87
  | [x] -> pp fmt x
88
  | _ -> fprintf fmt "(and @[<v 0>%a@]@ )" (Utils.fprintf_list ~sep:" " pp) l
89

    
90

    
91

    
92
let concat prefix x = if prefix = "" then x else prefix ^ "." ^ x
93
let rename f = (fun v -> {v with var_id = f v.var_id } )
94
let rename_machine p = rename (fun n -> concat p n)
95
let rename_machine_list p = List.map (rename_machine p)
96

    
97
let rename_current =  rename (fun n -> n ^ "_c")
98
let rename_current_list = List.map rename_current
99
let rename_next = rename (fun n -> n ^ "_x")
100
let rename_next_list = List.map rename_next
101

    
102

    
103
let get_machine machines node_name =
104
  List.find (fun m  -> m.mname.node_id = node_name) machines
105

    
106

    
107
let full_memory_vars machines machine =
108
  let rec aux fst prefix m =
109
    (rename_machine_list (if fst then prefix else concat prefix m.mname.node_id) m.mmemory) @
110
      List.fold_left (fun accu (id, (n, _)) ->
111
	let name = node_name n in
112
	if name = "_arrow" then accu else
113
	  let machine_n = get_machine machines name in
114
	  ( aux false (concat prefix (if fst then id else concat m.mname.node_id id)) machine_n ) @ accu
115
      ) [] (m.minstances)
116
  in
117
  aux true machine.mname.node_id machine
118

    
119

    
120
let stateless_vars machines m =
121
  (rename_machine_list m.mname.node_id m.mstep.step_inputs)@
122
    (rename_machine_list m.mname.node_id m.mstep.step_outputs)
123

    
124
let step_vars machines m =
125
  (stateless_vars machines m)@
126
    (rename_current_list (full_memory_vars machines m)) @
127
    (rename_next_list (full_memory_vars machines m))
128

    
129
let init_vars machines m =
130
  (stateless_vars machines m) @ (rename_next_list (full_memory_vars machines m))
131

    
132
(********************************************************************************************)
133
(*                    Instruction Printing functions                                        *)
134
(********************************************************************************************)
135

    
136
let pp_horn_var m fmt id =
137
(* PLOC TODO: array are printed as other variable 
138
   if Types.is_array_type id.var_type
139
  then
140
    assert false (* no arrays in Horn output *)
141
  else
142
*)   Format.fprintf fmt "%s" id.var_id
143

    
144

    
145
(* Used to print boolean constants *)
146
let pp_horn_tag fmt t =
147
  pp_print_string fmt (if t = tag_true then "true" else if t = tag_false then "false" else t)
148

    
149
(* Prints a constant value *)
150
let rec pp_horn_const fmt c =
151
  match c with
152
  | Const_int i    -> pp_print_int fmt i
153
  | Const_real r   -> pp_print_string fmt r
154
  | Const_float r  -> pp_print_float fmt r
155
  | Const_tag t    -> pp_horn_tag fmt t
156
  | Const_array ca -> assert false (* No constant arrays yet. We have to
157
				      introduce a dedicated constant array
158
				      builder *)
159
  | Const_string _ -> assert false (* String occurs in annotations *)
160
  | Const_struct _ ->assert false (* No struct yet in Horn *)
161

    
162
(* Prints a value expression [v], with internal function calls only.
163
   [pp_var] is a printer for variables (typically [pp_c_var_read]),
164
   but an offset suffix may be added for array variables
165
*)
166
let rec pp_horn_val ?(is_lhs=false) m self pp_var fmt v =
167
  match v with
168
    | Cst c         -> pp_horn_const fmt c
169
    | Array vl      -> 
170
      begin
171
	let array_multidim = get_array_instr_multidim v in
172
	fprintf fmt "%s" 
173
	  (build_array_string (pp_horn_val m self pp_var) (empty_array_var m array_multidim) vl)
174
      end
175
    | Access (t, i) -> 
176
      let pp = pp_horn_val ~is_lhs:is_lhs m self pp_var in
177
      fprintf fmt "(select %a %a)" pp t pp i 
178
    | Power (v, n)  -> assert false
179
    | LocalVar v    -> pp_var fmt (rename_machine self v)
180
    | StateVar v    ->
181
      if Types.is_array_type v.var_type
182
      then assert false
183
      else pp_var fmt (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v))
184
    | Fun (n, vl)   -> Format.fprintf fmt "%a" (Basic_library.pp_horn n (pp_horn_val m self pp_var)) vl
185

    
186
(* Prints a [value] indexed by the suffix list [loop_vars] *)
187
let rec pp_value_suffix m self pp_value fmt value =
188
 match value with
189
 | Fun (n, vl)  ->
190
   Basic_library.pp_horn n (pp_value_suffix m self pp_value) fmt vl
191
 |  _            ->
192
   pp_horn_val m self pp_value fmt value
193

    
194

    
195
      
196
(* type_directed assignment: array vs. statically sized type
197
   - [var_type]: type of variable to be assigned
198
   - [var_name]: name of variable to be assigned
199
   - [value]: assigned value
200
   - [pp_var]: printer for variables
201
*)
202
let pp_assign m self pp_var fmt var_type var_name value =
203
    fprintf fmt "(= %a %a)" 
204
      (pp_horn_val ~is_lhs:true m self pp_var) var_name 
205
      (pp_value_suffix m self pp_var) value
206

    
207
let pp_instance_call
208
    machines ?(init=false) m self fmt i (inputs: value_t list) (outputs: var_decl list) =
209
  try (* stateful node instance *)
210
    begin
211
      let (n,_) = List.assoc i m.minstances in
212
      match node_name n, inputs, outputs with
213
      | "_arrow", [i1; i2], [o] -> begin
214
        if init then
215
          pp_assign
216
   	    m
217
   	    self
218
   	    (pp_horn_var m)
219
	    fmt
220
   	    o.var_type (LocalVar o) i1
221
        else
222
          pp_assign
223
   	    m self (pp_horn_var m) fmt
224
   	    o.var_type (LocalVar o) i2
225

    
226
      end
227
      | name, _, _ ->
228
	begin
229
	  let target_machine = List.find (fun m  -> m.mname.node_id = name) machines in
230
	  if init then
231
	    Format.fprintf fmt "(%a %a%t%a%t%a)"
232
	      pp_machine_init_name (node_name n)
233
	      (* inputs *)
234
	      (Utils.fprintf_list ~sep:" " (pp_horn_val m self (pp_horn_var m)))
235
	      inputs
236
	      (Utils.pp_final_char_if_non_empty " " inputs)
237
	      (* outputs *)
238
	      (Utils.fprintf_list ~sep:" " (pp_horn_val m self (pp_horn_var m)))
239
	      (List.map (fun v -> LocalVar v) outputs)
240
	      (Utils.pp_final_char_if_non_empty " " outputs)
241
	      (* memories (next) *)
242
	      (Utils.fprintf_list ~sep:" " pp_var) (
243
  		rename_machine_list
244
		  (concat m.mname.node_id i)
245
		  (rename_next_list (full_memory_vars machines target_machine)
246
		  )
247
	       )
248
	  else
249
	    Format.fprintf fmt "(%a %a%t%a%t%a)"
250
	      pp_machine_step_name (node_name n)
251
	      (Utils.fprintf_list ~sep:" " (pp_horn_val m self (pp_horn_var m))) inputs
252
	      (Utils.pp_final_char_if_non_empty " " inputs)
253
	      (Utils.fprintf_list ~sep:" " (pp_horn_val m self (pp_horn_var m)))
254
	      (List.map (fun v -> LocalVar v) outputs)
255
	      (Utils.pp_final_char_if_non_empty " " outputs)
256
	      (Utils.fprintf_list ~sep:" " pp_var) (
257
		(rename_machine_list
258
		   (concat m.mname.node_id i)
259
		   (rename_current_list (full_memory_vars machines target_machine))
260
		) @
261
		  (rename_machine_list
262
		     (concat m.mname.node_id i)
263
		     (rename_next_list (full_memory_vars machines target_machine))
264
		  )
265
	       )
266

    
267
	end
268
    end
269
    with Not_found -> ( (* stateless node instance *)
270
      let (n,_) = List.assoc i m.mcalls in
271
      Format.fprintf fmt "(%s %a%t%a)"
272
	(node_name n)
273
	(Utils.fprintf_list ~sep:" " (pp_horn_val m self (pp_horn_var m)))
274
	inputs
275
	(Utils.pp_final_char_if_non_empty " " inputs)
276
	(Utils.fprintf_list ~sep:" " (pp_horn_val m self (pp_horn_var m)))
277
	(List.map (fun v -> LocalVar v) outputs)
278
    )
279

    
280
let pp_machine_init (m: machine_t) self fmt inst =
281
  let (node, static) = List.assoc inst m.minstances in
282
  fprintf fmt "(%a %a%t%s->%s)"
283
    pp_machine_init_name (node_name node)
284
    (Utils.fprintf_list ~sep:" " Dimension.pp_dimension) static
285
    (Utils.pp_final_char_if_non_empty " " static)
286
    self inst
287

    
288
(* TODO *)
289
let rec pp_conditional machines ?(init=false)  (m: machine_t) self fmt c tl el =
290
  fprintf fmt "@[<v 2>if (%a) {%t%a@]@,@[<v 2>} else {%t%a@]@,}"
291
    (pp_horn_val m self (pp_horn_var m)) c
292
    (Utils.pp_newline_if_non_empty tl)
293
    (Utils.fprintf_list ~sep:"@," (pp_machine_instr machines ~init:init  m self)) tl
294
    (Utils.pp_newline_if_non_empty el)
295
    (Utils.fprintf_list ~sep:"@," (pp_machine_instr machines ~init:init  m self)) el
296

    
297
and pp_machine_instr machines ?(init=false) (m: machine_t) self fmt instr =
298
  match instr with
299
  | MReset i ->
300
    pp_machine_init m self fmt i
301
  | MLocalAssign (i,v) ->
302
    pp_assign
303
      m self (pp_horn_var m) fmt
304
      i.var_type (LocalVar i) v
305
  | MStateAssign (i,v) ->
306
    pp_assign
307
      m self (pp_horn_var m) fmt
308
      i.var_type (StateVar i) v
309
  | MStep ([i0], i, vl) when Basic_library.is_internal_fun i  ->
310
    assert false (* This should not happen anymore *)
311
  | MStep (il, i, vl) ->
312
    pp_instance_call machines ~init:init m self fmt i vl il
313
  | MBranch (g,hl) ->
314
    if hl <> [] && let t = fst (List.hd hl) in t = tag_true || t = tag_false
315
    then (* boolean case, needs special treatment in C because truth value is not unique *)
316
      (* may disappear if we optimize code by replacing last branch test with default *)
317
      let tl = try List.assoc tag_true  hl with Not_found -> [] in
318
      let el = try List.assoc tag_false hl with Not_found -> [] in
319
      pp_conditional machines ~init:init m self fmt g tl el
320
    else assert false (* enum type case *)
321

    
322

    
323
(**************************************************************)
324

    
325
let is_stateless m = m.minstances = [] && m.mmemory = []
326

    
327
(* Print the machine m:
328
   two functions: m_init and m_step
329
   - m_init is a predicate over m memories
330
   - m_step is a predicate over old_memories, inputs, new_memories, outputs
331
   We first declare all variables then the two /rules/.
332

    
333
   For all arrays type, either inputs, outputs, state vars or local ones, we
334
   introduce an empty array variable: {machine_name}_array_x with x the dimension.
335
*)
336
let print_machine machines fmt m =
337
  let pp_instr init = pp_machine_instr machines ~init:init m in
338
  if m.mname.node_id = arrow_id then
339
    (* We don't print arrow function *)
340
    ()
341
  else
342
    begin
343
      Format.fprintf fmt "; %s@." m.mname.node_id;
344

    
345
   (* Printing variables *)
346
   Utils.fprintf_list ~sep:"@." pp_decl_var fmt
347
     ((step_vars machines m)@
348
	 (rename_machine_list m.mname.node_id m.mstep.step_locals));
349
   Format.pp_print_newline fmt ();
350

    
351
   (* Printing array empty val *)
352
   (* We gather required dimension and print the empty vars *)
353
   let required_empty_vars, _ = 
354
     List.fold_left (
355
       fun ((accu_var, accu_dim) as accu) vd ->
356
      (* If vd is an array, we may have to add an element to accu *)
357
	 if Types.is_array_type vd.var_type then
358
	   (* We compute the dimension width (???) of the array, ie. array is 1 vs
359
	      matrix is 2 vs 3D matrix is 3 , etc *)
360
	   let dim_size = Types.multidim vd.var_type in
361
	   if List.mem dim_size accu_dim then
362
	     (* this dimension was already computed. Do nothing *)
363
	     accu
364
	   else (* We create a new empty var, copying vd and changing its
365
		   name. We do not care for actual dimension, ie. size of
366
		   arrays *)
367
	     let new_var = {vd with var_id = empty_array_var m dim_size } in
368
	     new_var::accu_var, dim_size::accu_dim
369
	 else (* other wise do nothing *)
370
	   accu
371
     ) ([], []) (m.mstep.step_locals@m.mstep.step_inputs@m.mstep.step_outputs)
372
   in
373
   Utils.fprintf_list ~sep:"@." pp_decl_var fmt 
374
     required_empty_vars;
375
   Format.pp_print_newline fmt ();
376
 
377
   if is_stateless m then
378
     begin
379
       (* Declaring single predicate *)
380
       Format.fprintf fmt "(declare-rel %a (%a))@."
381
	 pp_machine_stateless_name m.mname.node_id
382
	 (Utils.fprintf_list ~sep:" " pp_horn_type)
383
	 (List.map (fun v -> v.var_type) (stateless_vars machines m));
384

    
385
       (* Rule for single predicate *)
386
       Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@."
387
	 (pp_conj (pp_instr
388
		     true (* In this case, the boolean init can be set to true or false.
389
			     The node is stateless. *)
390
		     m.mname.node_id)
391
	 )
392
	 m.mstep.step_instrs
393
	 pp_machine_stateless_name m.mname.node_id
394
	 (Utils.fprintf_list ~sep:" " pp_var) (stateless_vars machines m);
395
     end
396
   else
397
     begin
398
       (* Declaring predicate *)
399
       Format.fprintf fmt "(declare-rel %a (%a))@."
400
	 pp_machine_init_name m.mname.node_id
401
	 (Utils.fprintf_list ~sep:" " pp_horn_type)
402
	 (List.map (fun v -> v.var_type) (init_vars machines m));
403

    
404
       Format.fprintf fmt "(declare-rel %a (%a))@."
405
	 pp_machine_step_name m.mname.node_id
406
	 (Utils.fprintf_list ~sep:" " pp_horn_type)
407
	 (List.map (fun v -> v.var_type) (step_vars machines m));
408

    
409
       Format.pp_print_newline fmt ();
410

    
411
       (* Rule for init *)
412
       Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@."
413
	 (pp_conj (pp_instr true m.mname.node_id)) m.mstep.step_instrs
414
	 pp_machine_init_name m.mname.node_id
415
	 (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m);
416

    
417
      (* Adding assertions *)
418
       (match m.mstep.step_asserts with
419
       | [] ->
420
          begin
421
            (* Rule for init *)
422
            Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@."
423
	                   (pp_conj (pp_instr true m.mname.node_id)) m.mstep.step_instrs
424
	                   pp_machine_init_name m.mname.node_id
425
	                   (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m);
426
            (* Rule for step*)
427
            Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@."
428
                           (pp_conj (pp_instr false m.mname.node_id)) m.mstep.step_instrs
429
                           pp_machine_step_name m.mname.node_id
430
                           (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m);
431
          end
432
       | assertsl ->
433
          begin
434
	    let pp_val = pp_horn_val ~is_lhs:true m m.mname.node_id pp_var in
435
            (* print_string pp_val; *)
436
            let instrs_concat = m.mstep.step_instrs in
437
            Format.fprintf fmt "; with Assertions @.";
438
            (*Rule for init*)
439
            Format.fprintf fmt "@[<v 2>(rule (=> @ (and @ %a@. %a)(%a %a)@]@.))@.@."
440
                           (pp_conj (pp_instr true m.mname.node_id)) instrs_concat
441
                           (pp_conj pp_val) assertsl
442
                           pp_machine_init_name m.mname.node_id
443
                           (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m);
444
            (*Rule for step*)
445
            Format.fprintf fmt "@[<v 2>(rule (=> @ (and @ %a@. %a)(%a %a)@]@.))@.@."
446
                           (pp_conj (pp_instr false m.mname.node_id)) instrs_concat
447
                           (pp_conj pp_val) assertsl
448
                           pp_machine_step_name m.mname.node_id
449
                           (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m);
450
          end
451
       );
452
     end
453
    end
454

    
455

    
456

    
457
let collecting_semantics machines fmt node machine =
458
    Format.fprintf fmt "; Collecting semantics for node %s@.@." node;
459
    (* We print the types of the main node "memory tree" TODO: add the output *)
460
    let main_output =
461
     rename_machine_list machine.mname.node_id machine.mstep.step_outputs
462
    in
463
    let main_output_dummy =
464
     rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_outputs
465
    in
466
    let main_memory_next =
467
      (rename_next_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @
468
      main_output
469
    in
470
    let main_memory_current =
471
      (rename_current_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @
472
      main_output_dummy
473
    in
474

    
475
    (* Special case when the main node is stateless *)
476
    let init_name, step_name =
477
      if is_stateless machine then
478
	pp_machine_stateless_name, pp_machine_stateless_name
479
      else
480
	pp_machine_init_name, pp_machine_step_name
481
    in
482

    
483
    Format.fprintf fmt "(declare-rel MAIN (%a))@."
484
      (Utils.fprintf_list ~sep:" " pp_horn_type)
485
      (List.map (fun v -> v.var_type) main_memory_next);
486

    
487
    Format.fprintf fmt "; Initial set@.";
488
    Format.fprintf fmt "(declare-rel INIT_STATE ())@.";
489
    Format.fprintf fmt "(rule INIT_STATE)@.";
490
    Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>INIT_STATE@ (@[<v 0>%a %a@])@]@ )@ (MAIN %a)@]@.))@.@."
491
      init_name node
492
      (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines machine)
493
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_next ;
494

    
495
    Format.fprintf fmt "; Inductive def@.";
496
    (Utils.fprintf_list ~sep:" " (fun fmt v -> Format.fprintf fmt "%a@." pp_decl_var v)) fmt main_output_dummy;
497
    Format.fprintf fmt
498
      "@[<v 2>(rule (=> @ (and @[<v 0>(MAIN %a)@ (@[<v 0>%a %a@])@]@ )@ (MAIN %a)@]@.))@.@."
499
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_current
500
      step_name node
501
      (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines machine)
502
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_next
503

    
504
let check_prop machines fmt node machine =
505
  let main_output =
506
    rename_machine_list machine.mname.node_id machine.mstep.step_outputs
507
  in
508
  let main_memory_next =
509
    (rename_next_list (full_memory_vars machines machine)) @ main_output
510
  in
511
  Format.fprintf fmt "; Property def@.";
512
  Format.fprintf fmt "(declare-rel ERR ())@.";
513
  Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (MAIN %a)@])@ ERR))@."
514
    (pp_conj pp_var) main_output
515
    (Utils.fprintf_list ~sep:" " pp_var) main_memory_next
516
    ;
517
   if !Options.horn_query then Format.fprintf fmt "(query ERR)@."
518

    
519

    
520
let cex_computation machines fmt node machine =
521
    Format.fprintf fmt "; CounterExample computation for node %s@.@." node;
522
    (* We print the types of the cex node "memory tree" TODO: add the output *)
523
    let cex_input =
524
     rename_machine_list machine.mname.node_id machine.mstep.step_inputs
525
    in
526
    let cex_input_dummy =
527
     rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_inputs
528
    in
529
    let cex_output =
530
     rename_machine_list machine.mname.node_id machine.mstep.step_outputs
531
    in
532
    let cex_output_dummy =
533
     rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_outputs
534
    in
535
    let cex_memory_next =
536
      cex_input @ (rename_next_list (full_memory_vars machines machine)) @ cex_output
537
    in
538
    let cex_memory_current =
539
      cex_input_dummy @ (rename_current_list (full_memory_vars machines machine)) @ cex_output_dummy
540
    in
541

    
542
    (* Special case when the cex node is stateless *)
543
    let init_name, step_name =
544
      if is_stateless machine then
545
	pp_machine_stateless_name, pp_machine_stateless_name
546
      else
547
	pp_machine_init_name, pp_machine_step_name
548
    in
549

    
550
    Format.fprintf fmt "(declare-rel CEX (Int %a))@.@."
551
      (Utils.fprintf_list ~sep:" " pp_horn_type)
552
      (List.map (fun v -> v.var_type) cex_memory_next);
553

    
554
    Format.fprintf fmt "; Initial set@.";
555
    Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>INIT_STATE@ (@[<v 0>%a %a@])@]@ )@ (CEX 0 %a)@]@.))@.@."
556
      init_name node
557
      (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines machine)
558
      (Utils.fprintf_list ~sep:" " pp_var) cex_memory_next ;
559

    
560
    Format.fprintf fmt "; Inductive def@.";
561
    (* Declare dummy inputs. Outputs should have been declared previously with collecting sem *)
562
    (Utils.fprintf_list ~sep:" " (fun fmt v -> Format.fprintf fmt "%a@." pp_decl_var v)) fmt cex_input_dummy;
563
    Format.fprintf fmt "(declare-var cexcpt Int)@.";
564
    Format.fprintf fmt
565
      "@[<v 2>(rule (=> @ (and @[<v 0>(CEX cexcpt %a)@ (@[<v 0>%a %a@])@]@ )@ (CEX (+ 1 cexcpt) %a)@]@.))@.@."
566
      (Utils.fprintf_list ~sep:" " pp_var) cex_memory_current
567
      step_name node
568
      (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines machine)
569
      (Utils.fprintf_list ~sep:" " pp_var) cex_memory_next
570

    
571
let get_cex machines fmt node machine =
572
    let cex_input =
573
     rename_machine_list machine.mname.node_id machine.mstep.step_inputs
574
    in
575
    let cex_output =
576
     rename_machine_list machine.mname.node_id machine.mstep.step_outputs
577
    in
578
  let cex_memory_next =
579
    cex_input @ (rename_next_list (full_memory_vars machines machine)) @ cex_output
580
  in
581
  Format.fprintf fmt "; Property def@.";
582
  Format.fprintf fmt "(declare-rel CEXTRACE ())@.";
583
  Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (CEX cexcpt %a)@])@ CEXTRACE))@."
584
    (pp_conj pp_var) cex_output
585
    (Utils.fprintf_list ~sep:" " pp_var) cex_memory_next
586
    ;
587
  Format.fprintf fmt "(query CEXTRACE)@."
588

    
589

    
590
let main_print machines fmt =
591
if !Options.main_node <> "" then
592
  begin
593
    let node = !Options.main_node in
594
    let machine = get_machine machines node in
595

    
596

    
597
    collecting_semantics machines fmt node machine;
598
    check_prop machines fmt node machine;
599
    if !Options.horn_cex then(
600
      cex_computation machines fmt node machine;
601
      get_cex machines fmt node machine)
602
end
603

    
604
let print_const_def fmt cdecl =
605
  (* Declare var with appropriate type *)
606
  fprintf fmt "(declare-const %s %a);@."
607
    cdecl.const_id 
608
    pp_horn_type cdecl.const_type;
609
  (* Assert its value. Special treatment for array constants *)
610
  match cdecl.const_value, (Types.repr cdecl.const_type).Types.tdesc with
611
  | Const_array cl, Types.Tstatic _  -> 
612
    fprintf fmt "(assert (= %s %s));@."
613
      cdecl.const_id
614
      (build_array_string pp_horn_const cdecl.const_id cl)
615

    
616
  | _ -> 
617
    fprintf fmt "(assert (= %s %a));@." 
618
      cdecl.const_id
619
      pp_horn_const cdecl.const_value 
620
      
621

    
622
let translate fmt basename prog machines =
623
  (* Print consts *)
624
  fprintf fmt "; Global constants (definitions) @.";
625
  fprintf fmt "@[<v>";
626
  List.iter (fun c -> print_const_def fmt (const_of_top c)) (get_consts prog);
627
  fprintf fmt "@]@.";
628

    
629
  (* Print machines *)
630
  List.iter (print_machine machines fmt) (List.rev machines);
631

    
632
  (* Print main *)
633
  main_print machines fmt
634

    
635

    
636
let traces_file fmt basename prog machines =
637

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

    
641
  (* We extract the annotation dealing with traceability *)
642
  let machines_traces = List.map (fun m ->
643
    let traces : (ident * expr) list=
644
      let all_annots = List.flatten (List.map (fun ann -> ann.annots) m.mannot) in
645
      let filtered =
646
	List.filter (fun (kwds, _) -> kwds = ["traceability"]) all_annots
647
      in
648
      let content = List.map snd filtered in
649
      (* Elements are supposed to be a pair (tuple): variable, expression *)
650
      List.map (fun ee ->
651
	match ee.eexpr_quantifiers, ee.eexpr_qfexpr.expr_desc with
652
	| [], Expr_tuple [v;e] -> (
653
	  match v.expr_desc with
654
	  | Expr_ident vid -> vid, e
655
	  | _ -> assert false )
656
	| _ -> assert false)
657
	content
658
    in
659

    
660
    m, traces
661

    
662
  ) machines
663
  in
664

    
665
  (* Compute memories associated to each machine *)
666
  let compute_mems m =
667
    let rec aux fst prefix m =
668
      (List.map (fun mem -> (prefix, mem)) m.mmemory) @
669
	List.fold_left (fun accu (id, (n, _)) ->
670
	  let name = node_name n in
671
	  if name = "_arrow" then accu else
672
	    let machine_n = get_machine machines name in
673
	    ( aux false ((id,machine_n)::prefix) machine_n )
674
	    @ accu
675
	) [] m.minstances
676
    in
677
    aux true [] m
678
  in
679

    
680
  List.iter (fun m ->
681
    (* Format.fprintf fmt "; Node %s@." m.mname.node_id; *)
682
    Format.fprintf fmt "    <Node name=\"%s\">@." m.mname.node_id;
683

    
684
    let memories_old =
685
      List.map (fun (p, v) ->
686
	let machine = match p with | [] -> m | (_,m')::_ -> m' in
687
	let traces = List.assoc machine machines_traces in
688
	if List.mem_assoc v.var_id traces then (
689
	  (* We take the expression associated to variable v in the trace info *)
690
	  (* Format.eprintf "Found variable %a in traces: %a@."  pp_var v Printers.pp_expr (List.assoc v.var_id traces); *)
691
	  p, List.assoc v.var_id traces
692
      )
693
	else (
694
	  (* We keep the variable as is: we create an expression v *)
695
	  (* 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); *)
696
	  p, mkexpr Location.dummy_loc (Expr_ident v.var_id)
697
	)
698

    
699
      ) (compute_mems m)
700
    in
701
    let memories_next = (* We remove the topest pre in each expression *)
702
      List.map
703
      	(fun (prefix, ee) ->
704
      	  match ee.expr_desc with
705
      	  | Expr_pre e -> prefix, e
706
      	  | _ -> Format.eprintf
707
      	    "Mem Failure: (prefix: %a, eexpr: %a)@.@?"
708
      	    (Utils.fprintf_list ~sep:","
709
      	       (fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id ))
710
      	    (List.rev prefix)
711
      	    Printers.pp_expr ee;
712
      	    assert false)
713
	memories_old
714
    in
715

    
716
    (* let pp_prefix_rev fmt prefix = *)
717
    (*   Utils.fprintf_list ~sep:"." (fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id) fmt (List.rev prefix) *)
718
    (* in *)
719

    
720
    let pp_prefix_rev fmt prefix =
721
      Utils.fprintf_list ~sep:"." (fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id) fmt (List.rev prefix)
722
    in
723

    
724
    let input_vars = (rename_machine_list m.mname.node_id m.mstep.step_inputs) in
725
    let output_vars = (rename_machine_list m.mname.node_id m.mstep.step_outputs) in
726
     Format.fprintf fmt "     <input name=\"%a\" type=\"%a\">%a</input> @."
727
                   (Utils.fprintf_list ~sep:" | " pp_var) input_vars
728
                   (Utils.fprintf_list ~sep:" | "  (fun fmt id -> pp_horn_type fmt id.var_type)) input_vars
729
                   (Utils.fprintf_list ~sep:" | " pp_var) (m.mstep.step_inputs);
730

    
731
    Format.fprintf fmt "      <output name=\"%a\" type=\"%a\">%a</output> @."
732
                   (Utils.fprintf_list ~sep:" | " pp_var)  output_vars
733
                   (Utils.fprintf_list ~sep:" | "  (fun fmt id -> pp_horn_type fmt id.var_type)) output_vars
734
                   (Utils.fprintf_list ~sep:" | " pp_var) (m.mstep.step_outputs);
735

    
736
    let init_local_vars = (rename_next_list (full_memory_vars machines m)) in
737
    let step_local_vars = (rename_current_list (full_memory_vars machines m)) in
738

    
739
    Format.fprintf fmt "      <localInit name=\"%a\" type=\"%a\">%t%a</localInit> @."
740
                   (Utils.fprintf_list ~sep:" | " pp_var) init_local_vars
741
                   (Utils.fprintf_list ~sep:" | "  (fun fmt id -> pp_horn_type fmt id.var_type)) init_local_vars
742
                   (fun fmt -> match memories_next with [] -> () | _ -> fprintf fmt "")
743
                   (Utils.fprintf_list ~sep:" | " (fun fmt (prefix, ee) -> fprintf fmt "%a" Printers.pp_expr ee)) memories_next;
744

    
745
    Format.fprintf fmt "      <localStep name=\"%a\" type=\"%a\">%t%a</localStep> @."
746
                   (Utils.fprintf_list ~sep:" | " pp_var) step_local_vars
747
                   (Utils.fprintf_list ~sep:" | "  (fun fmt id -> pp_horn_type fmt id.var_type)) step_local_vars
748
                   (fun fmt -> match memories_old with [] -> () | _ -> fprintf fmt "")
749
                     (Utils.fprintf_list ~sep:" | " (fun fmt (prefix,ee) -> fprintf fmt "(%a)"
750
                                    Printers.pp_expr ee)) (memories_old);
751

    
752
     Format.fprintf fmt "    </Node>@.";
753

    
754
  ) (List.rev machines);
755
  Format.fprintf fmt "</Traces>@.";
756

    
757
          (* (Utils.fprintf_list ~sep:" | " (fun fmt (prefix, ee) -> fprintf fmt "%a%a" pp_prefix_rev prefix Printers.pp_expr ee)) memories_next; *)
758
   (* (Utils.fprintf_list ~sep:" | " (fun fmt (prefix,ee) -> fprintf fmt "%a(%a)" *)
759
   (*                                  pp_prefix_rev prefix Printers.pp_expr ee)) (memories_old); *)
760

    
761
(* Local Variables: *)
762
(* compile-command:"make -C ../.." *)
763
(* End: *)