Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / backends / Horn / horn_backend.ml @ 3ca6d126

History | View | Annotate | Download (25.2 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 pp_type fmt t =
26
  match (Types.repr t).Types.tdesc with
27
  | Types.Tbool           -> Format.fprintf fmt "Bool"
28
  | Types.Tint            -> Format.fprintf fmt "Int"
29
  | Types.Treal           -> Format.fprintf fmt "Real"
30
  | Types.Tclock _
31
  | Types.Tarray _
32
  | Types.Tstatic _
33
  | Types.Tconst _
34
  | Types.Tarrow _
35
  | _                     -> Format.eprintf "internal error: pp_type %a@."
36
    Types.print_ty t; assert false
37

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

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

    
45

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

    
52

    
53

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

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

    
64

    
65
let get_machine machines node_name =
66
  List.find (fun m  -> m.mname.node_id = node_name) machines
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
let stateless_vars machines m =
81
  (rename_machine_list m.mname.node_id m.mstep.step_inputs)@
82
    (rename_machine_list m.mname.node_id m.mstep.step_outputs)
83

    
84
let step_vars machines m =
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

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

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

    
103

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

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

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

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

    
142
(* type_directed assignment: array vs. statically sized type
143
   - [var_type]: type of variable to be assigned
144
   - [var_name]: name of variable to be assigned
145
   - [value]: assigned value
146
   - [pp_var]: printer for variables
147
*)
148
let pp_assign m self pp_var fmt var_type var_name value =
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
152
    machines ?(init=false) m self fmt i (inputs: value_t list) (outputs: var_decl list) =
153
  try (* stateful node instance *)
154
    begin
155
      let (n,_) = List.assoc i m.minstances in
156
      match node_name n, inputs, outputs with
157
      | "_arrow", [i1; i2], [o] -> begin
158
        if init then
159
          pp_assign
160
   	    m
161
   	    self
162
   	    (pp_horn_var m)
163
	    fmt
164
   	    o.var_type (LocalVar o) i1
165
        else
166
          pp_assign
167
   	    m self (pp_horn_var m) fmt
168
   	    o.var_type (LocalVar o) i2
169

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

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

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

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

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

    
266

    
267
(**************************************************************)
268

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

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

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

    
292

    
293

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

    
302
       (* Rule for single predicate *)
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.
306
			     The node is stateless. *)
307
		     m.mname.node_id)
308
	 )
309
	 m.mstep.step_instrs
310
	 pp_machine_stateless_name m.mname.node_id
311
	 (Utils.fprintf_list ~sep:" " pp_var) (stateless_vars machines m);
312
     end
313
   else
314
     begin
315
       (* Declaring predicate *)
316
       Format.fprintf fmt "(declare-rel %a (%a))@."
317
	 pp_machine_init_name m.mname.node_id
318
	 (Utils.fprintf_list ~sep:" " pp_type)
319
	 (List.map (fun v -> v.var_type) (init_vars machines m));
320

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

    
326
       Format.pp_print_newline fmt ();
327

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

    
334
       (* (\* Rule for step *\) *)
335
       (* Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@." *)
336
       (*   (pp_conj (pp_instr false m.mname.node_id)) m.mstep.step_instrs *)
337
       (*   pp_machine_step_name m.mname.node_id *)
338
       (*   (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m); *)
339

    
340

    
341
        (* Adding assertions *)
342
       (match m.mstep.step_asserts with
343
       | [] ->
344
          begin
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

    
353
	    let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id pp_var in
354
            (* print_string pp_val; *)
355
            let instrs_concat = m.mstep.step_instrs in
356
            Format.fprintf fmt "; with Invariants @.";
357
            Format.fprintf fmt "@[<v 2>(rule (=> @ (and @ %a@. %a)(%a %a)@]@.))@.@."
358
                           (pp_conj (pp_instr false m.mname.node_id)) instrs_concat
359
                           (pp_conj pp_val) assertsl
360
                           pp_machine_step_name m.mname.node_id
361
                           (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m);
362

    
363

    
364
	    (* Format.fprintf fmt " @[<v 2>%a@]@ @.@.@." *)
365
            (*                 (pp_conj pp_val) assertsl; *)
366

    
367
          end
368
       );
369

    
370
       (* (\* Adding assertions *\) *)
371
       (* (match m.mstep.step_asserts with *)
372
       (* | [] -> () *)
373
       (* | assertsl -> begin *)
374
       (*   let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id pp_var in *)
375

    
376
       (*   Format.fprintf fmt "; Asserts@."; *)
377
       (*   Format.fprintf fmt "(assert @[<v 2>%a@]@ )@.@.@." *)
378
       (*     (pp_conj pp_val) assertsl; *)
379

    
380
       (*   (\** TEME: the following code is the one we described. But it generates a segfault in z3 *)
381
       (*   Format.fprintf fmt "; Asserts for init@."; *)
382
       (*   Format.fprintf fmt "@[<v 2>(assert (=> @ (and @[<v 0>%a@]@ (%a %a))@ %a@]@.))@.@.@." *)
383
       (*     (Utils.fprintf_list ~sep:"@ " (pp_instr true m.mname.node_id)) m.mstep.step_instrs *)
384
       (*     pp_machine_init_name m.mname.node_id *)
385
       (*     (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m) *)
386
       (*     (pp_conj pp_val) assertsl; *)
387

    
388
       (*   Format.fprintf fmt "; Asserts for step@."; *)
389
       (*   Format.fprintf fmt "@[<v 2>(assert (=> @ (and @[<v 0>%a@]@ (%a %a))@ %a@]@.))@.@." *)
390
       (*     (Utils.fprintf_list ~sep:"@ " (pp_instr false m.mname.node_id)) m.mstep.step_instrs *)
391

    
392
       (*     pp_machine_step_name m.mname.node_id *)
393
       (*     (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m) *)
394
       (*     (pp_conj pp_val) assertsl *)
395
       (*   *\) *)
396
       (* end *)
397
       (* ); *)
398

    
399
(*
400
       match m.mspec with
401
	 None -> () (* No node spec; we do nothing *)
402
       | Some {requires = []; ensures = [EnsuresExpr e]; behaviors = []} ->
403
	 (
404
       (* For the moment, we only deal with simple case: single ensures, no other parameters *)
405
	   ()
406

    
407
	 )
408
       | _ -> () (* Other cases give nothing *)
409
*)
410
     end
411
    end
412

    
413

    
414

    
415
let collecting_semantics machines fmt node machine =
416
    Format.fprintf fmt "; Collecting semantics for node %s@.@." node;
417
    (* We print the types of the main node "memory tree" TODO: add the output *)
418
    let main_output =
419
     rename_machine_list machine.mname.node_id machine.mstep.step_outputs
420
    in
421
    let main_output_dummy =
422
     rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_outputs
423
    in
424
    let main_memory_next =
425
      (rename_next_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @
426
      main_output
427
    in
428
    let main_memory_current =
429
      (rename_current_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @
430
      main_output_dummy
431
    in
432

    
433
    (* Special case when the main node is stateless *)
434
    let init_name, step_name =
435
      if is_stateless machine then
436
	pp_machine_stateless_name, pp_machine_stateless_name
437
      else
438
	pp_machine_init_name, pp_machine_step_name
439
    in
440

    
441
    Format.fprintf fmt "(declare-rel MAIN (%a))@."
442
      (Utils.fprintf_list ~sep:" " pp_type)
443
      (List.map (fun v -> v.var_type) main_memory_next);
444

    
445
    Format.fprintf fmt "; Initial set@.";
446
    Format.fprintf fmt "(declare-rel INIT_STATE ())@.";
447
    Format.fprintf fmt "(rule INIT_STATE)@.";
448
    Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>INIT_STATE@ (@[<v 0>%a %a@])@]@ )@ (MAIN %a)@]@.))@.@."
449
      init_name node
450
      (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines machine)
451
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_next ;
452

    
453
    Format.fprintf fmt "; Inductive def@.";
454
    (Utils.fprintf_list ~sep:" " (fun fmt v -> Format.fprintf fmt "%a@." pp_decl_var v)) fmt main_output_dummy;
455
    Format.fprintf fmt
456
      "@[<v 2>(rule (=> @ (and @[<v 0>(MAIN %a)@ (@[<v 0>%a %a@])@]@ )@ (MAIN %a)@]@.))@.@."
457
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_current
458
      step_name node
459
      (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines machine)
460
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_next
461

    
462
let check_prop machines fmt node machine =
463
  let main_output =
464
    rename_machine_list machine.mname.node_id machine.mstep.step_outputs
465
  in
466
  let main_memory_next =
467
    (rename_next_list (full_memory_vars machines machine)) @ main_output
468
  in
469
  Format.fprintf fmt "; Property def@.";
470
  Format.fprintf fmt "(declare-rel ERR ())@.";
471
  Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (MAIN %a)@])@ ERR))@."
472
    (pp_conj pp_var) main_output
473
    (Utils.fprintf_list ~sep:" " pp_var) main_memory_next
474
    ;
475
  if !Options.horn_queries then
476
    Format.fprintf fmt "(query ERR)@."
477

    
478

    
479
let cex_computation machines fmt node machine =
480
    Format.fprintf fmt "; CounterExample computation for node %s@.@." node;
481
    (* We print the types of the cex node "memory tree" TODO: add the output *)
482
    let cex_input =
483
     rename_machine_list machine.mname.node_id machine.mstep.step_inputs
484
    in
485
    let cex_input_dummy =
486
     rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_inputs
487
    in
488
    let cex_output =
489
     rename_machine_list machine.mname.node_id machine.mstep.step_outputs
490
    in
491
    let cex_output_dummy =
492
     rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_outputs
493
    in
494
    let cex_memory_next =
495
      cex_input @ (rename_next_list (full_memory_vars machines machine)) @ cex_output
496
    in
497
    let cex_memory_current =
498
      cex_input_dummy @ (rename_current_list (full_memory_vars machines machine)) @ cex_output_dummy
499
    in
500

    
501
    (* Special case when the cex node is stateless *)
502
    let init_name, step_name =
503
      if is_stateless machine then
504
	pp_machine_stateless_name, pp_machine_stateless_name
505
      else
506
	pp_machine_init_name, pp_machine_step_name
507
    in
508

    
509
    Format.fprintf fmt "(declare-rel CEX (Int %a))@.@."
510
      (Utils.fprintf_list ~sep:" " pp_type)
511
      (List.map (fun v -> v.var_type) cex_memory_next);
512

    
513
    Format.fprintf fmt "; Initial set@.";
514
    Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>INIT_STATE@ (@[<v 0>%a %a@])@]@ )@ (CEX 0 %a)@]@.))@.@."
515
      init_name node
516
      (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines machine)
517
      (Utils.fprintf_list ~sep:" " pp_var) cex_memory_next ;
518

    
519
    Format.fprintf fmt "; Inductive def@.";
520
    (* Declare dummy inputs. Outputs should have been declared previously with collecting sem *)
521
    (Utils.fprintf_list ~sep:" " (fun fmt v -> Format.fprintf fmt "%a@." pp_decl_var v)) fmt cex_input_dummy;
522
    Format.fprintf fmt "(declare-var cexcpt Int)@.";
523
    Format.fprintf fmt
524
      "@[<v 2>(rule (=> @ (and @[<v 0>(CEX cexcpt %a)@ (@[<v 0>%a %a@])@]@ )@ (CEX (+ 1 cexcpt) %a)@]@.))@.@."
525
      (Utils.fprintf_list ~sep:" " pp_var) cex_memory_current
526
      step_name node
527
      (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines machine)
528
      (Utils.fprintf_list ~sep:" " pp_var) cex_memory_next
529

    
530
let get_cex machines fmt node machine =
531
    let cex_input =
532
     rename_machine_list machine.mname.node_id machine.mstep.step_inputs
533
    in
534
    let cex_output =
535
     rename_machine_list machine.mname.node_id machine.mstep.step_outputs
536
    in
537
  let cex_memory_next =
538
    cex_input @ (rename_next_list (full_memory_vars machines machine)) @ cex_output
539
  in
540
  Format.fprintf fmt "; Property def@.";
541
  Format.fprintf fmt "(declare-rel CEXTRACE ())@.";
542
  Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (CEX cexcpt %a)@])@ CEXTRACE))@."
543
    (pp_conj pp_var) cex_output
544
    (Utils.fprintf_list ~sep:" " pp_var) cex_memory_next
545
    ;
546
  if !Options.horn_queries then
547
    Format.fprintf fmt "(query CEXTRACE)@."
548

    
549

    
550
let main_print machines fmt =
551
if !Options.main_node <> "" then
552
  begin
553
    let node = !Options.main_node in
554
    let machine = get_machine machines node in
555

    
556

    
557
    collecting_semantics machines fmt node machine;
558
    check_prop machines fmt node machine;
559
    if !Options.horn_cex then(
560
      cex_computation machines fmt node machine;
561
      get_cex machines fmt node machine)
562
end
563

    
564

    
565
let translate fmt basename prog machines =
566
  List.iter (print_machine machines fmt) (List.rev machines);
567
  main_print machines fmt
568

    
569

    
570
let traces_file fmt basename prog machines =
571
  Format.fprintf fmt
572
    "; Horn code traceability generated by %s@.; SVN version number %s@.@."
573
    (Filename.basename Sys.executable_name)
574
    Version.number;
575

    
576
  (* We extract the annotation dealing with traceability *)
577
  let machines_traces = List.map (fun m ->
578
    let traces : (ident * expr) list=
579
      let all_annots = List.flatten (List.map (fun ann -> ann.annots) m.mannot) in
580
      let filtered =
581
	List.filter (fun (kwds, _) -> kwds = ["traceability"]) all_annots
582
      in
583
      let content = List.map snd filtered in
584
      (* Elements are supposed to be a pair (tuple): variable, expression *)
585
      List.map (fun ee ->
586
	match ee.eexpr_quantifiers, ee.eexpr_qfexpr.expr_desc with
587
	| [], Expr_tuple [v;e] -> (
588
	  match v.expr_desc with
589
	  | Expr_ident vid -> vid, e
590
	  | _ -> assert false )
591
	| _ -> assert false)
592
	content
593
    in
594

    
595
    m, traces
596

    
597
  ) machines
598
  in
599

    
600
  (* Compute memories associated to each machine *)
601
  let compute_mems m =
602
    let rec aux fst prefix m =
603
      (List.map (fun mem -> (prefix, mem)) m.mmemory) @
604
	List.fold_left (fun accu (id, (n, _)) ->
605
	  let name = node_name n in
606
	  if name = "_arrow" then accu else
607
	    let machine_n = get_machine machines name in
608
	    ( aux false ((id,machine_n)::prefix) machine_n )
609
	    @ accu
610
	) [] m.minstances
611
    in
612
    aux true [] m
613
  in
614

    
615
  List.iter (fun m ->
616
    Format.fprintf fmt "; Node %s@." m.mname.node_id;
617

    
618
    let memories_old =
619
      List.map (fun (p, v) ->
620
	let machine = match p with | [] -> m | (_,m')::_ -> m' in
621
	let traces = List.assoc machine machines_traces in
622
	if List.mem_assoc v.var_id traces then (
623
	  (* We take the expression associated to variable v in the trace info *)
624
	  (* Format.eprintf "Found variable %a in traces: %a@."  pp_var v Printers.pp_expr (List.assoc v.var_id traces); *)
625
	  p, List.assoc v.var_id traces
626
      )
627
	else (
628
	  (* We keep the variable as is: we create an expression v *)
629
	  (* 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); *)
630
	  p, mkexpr Location.dummy_loc (Expr_ident v.var_id)
631
	)
632

    
633
      ) (compute_mems m)
634
    in
635
    let memories_next = (* We remove the topest pre in each expression *)
636
      List.map
637
      	(fun (prefix, ee) ->
638
      	  match ee.expr_desc with
639
      	  | Expr_pre e -> prefix, e
640
      	  | _ -> Format.eprintf
641
      	    "Mem Failure: (prefix: %a, eexpr: %a)@.@?"
642
      	    (Utils.fprintf_list ~sep:","
643
      	       (fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id ))
644
      	    (List.rev prefix)
645
      	    Printers.pp_expr ee;
646
      	    assert false)
647
	memories_old
648
    in
649

    
650
    let pp_prefix_rev fmt prefix =
651
      Utils.fprintf_list ~sep:"." (fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id) fmt (List.rev prefix)
652
    in
653

    
654
    Format.fprintf fmt "; Init predicate@.";
655

    
656
    Format.fprintf fmt "; horn encoding@.";
657
    Format.fprintf fmt "(%a %a)@."
658
      pp_machine_init_name m.mname.node_id
659
      (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m);
660

    
661
    Format.fprintf fmt "; original expressions@.";
662
    Format.fprintf fmt "(%a %a%t%a)@."
663
      pp_machine_init_name m.mname.node_id
664
      (Utils.fprintf_list ~sep:" " pp_var) (m.mstep.step_inputs@m.mstep.step_outputs)
665
      (fun fmt -> match memories_next with [] -> () | _ -> fprintf fmt " ")
666
      (Utils.fprintf_list ~sep:" " (fun fmt (prefix, ee) -> fprintf fmt "%a(%a)" pp_prefix_rev prefix Printers.pp_expr ee)) memories_next;
667

    
668
    Format.pp_print_newline fmt ();
669
    Format.fprintf fmt "; Step predicate@.";
670

    
671
    Format.fprintf fmt "; horn encoding@.";
672
    Format.fprintf fmt "(%a %a)@."
673
      pp_machine_step_name m.mname.node_id
674
      (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m);
675
    Format.fprintf fmt "; original expressions@.";
676
    Format.fprintf fmt "(%a %a%t%a)@."
677
      pp_machine_step_name m.mname.node_id
678
      (Utils.fprintf_list ~sep:" " pp_var) (m.mstep.step_inputs@m.mstep.step_outputs)
679
      (fun fmt -> match memories_old with [] -> () | _ -> fprintf fmt " ")
680
      (Utils.fprintf_list ~sep:" " (fun fmt (prefix,ee) -> fprintf fmt "%a(%a)" pp_prefix_rev prefix Printers.pp_expr ee)) (memories_old@memories_next);
681
    Format.pp_print_newline fmt ();
682
  ) (List.rev machines);
683

    
684

    
685
(* Local Variables: *)
686
(* compile-command:"make -C ../.." *)
687
(* End: *)