Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / backends / Horn / horn_backend.ml @ 7c95dcab

History | View | Annotate | Download (26.5 KB)

1 96d33ff2 tkahsai
(********************************************************************)
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 7c95dcab ploc
let rec pp_type fmt t =
26 96d33ff2 tkahsai
  match (Types.repr t).Types.tdesc with
27 7c95dcab ploc
  | Types.Tbool           -> fprintf fmt "Bool"
28
  | Types.Tint            -> fprintf fmt "Int"
29
  | Types.Treal           -> fprintf fmt "Real"
30
  | Types.Tconst ty       -> pp_print_string fmt ty
31
  | Types.Tclock t        -> pp_type fmt t
32 96d33ff2 tkahsai
  | Types.Tarray _
33
  | Types.Tstatic _
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
69
let full_memory_vars machines machine =
70
  let rec aux fst prefix m =
71
    (rename_machine_list (if fst then prefix else concat prefix m.mname.node_id) m.mmemory) @
72
      List.fold_left (fun accu (id, (n, _)) ->
73
	let name = node_name n in
74
	if name = "_arrow" then accu else
75
	  let machine_n = get_machine machines name in
76
	  ( aux false (concat prefix (if fst then id else concat m.mname.node_id id)) machine_n ) @ accu
77
      ) [] (m.minstances)
78
  in
79
  aux true machine.mname.node_id machine
80
81
82
let stateless_vars machines m =
83
  (rename_machine_list m.mname.node_id m.mstep.step_inputs)@
84
    (rename_machine_list m.mname.node_id m.mstep.step_outputs)
85
86
let step_vars machines m =
87
  (stateless_vars machines m)@
88
    (rename_current_list (full_memory_vars machines m)) @
89
    (rename_next_list (full_memory_vars machines m))
90
91
let init_vars machines m =
92
  (stateless_vars machines m) @ (rename_next_list (full_memory_vars machines m))
93
94
(********************************************************************************************)
95
(*                    Instruction Printing functions                                        *)
96
(********************************************************************************************)
97
98
let pp_horn_var m fmt id =
99
  if Types.is_array_type id.var_type
100
  then
101
    assert false (* no arrays in Horn output *)
102
  else
103
    Format.fprintf fmt "%s" id.var_id
104
105
106
(* Used to print boolean constants *)
107
let pp_horn_tag fmt t =
108
  pp_print_string fmt (if t = tag_true then "true" else if t = tag_false then "false" else t)
109
110
(* Prints a constant value *)
111
let rec pp_horn_const fmt c =
112
  match c with
113
    | Const_int i    -> pp_print_int fmt i
114
    | Const_real r   -> pp_print_string fmt r
115
    | Const_float r  -> pp_print_float fmt r
116
    | Const_tag t    -> pp_horn_tag fmt t
117
    | _              -> assert false
118
119
(* Prints a value expression [v], with internal function calls only.
120
   [pp_var] is a printer for variables (typically [pp_c_var_read]),
121
   but an offset suffix may be added for array variables
122
*)
123
let rec pp_horn_val ?(is_lhs=false) self pp_var fmt v =
124
  match v with
125
    | Cst c         -> pp_horn_const fmt c
126
    | Array _
127
    | Access _ -> assert false (* no arrays *)
128
    | Power (v, n)  -> assert false
129
    | LocalVar v    -> pp_var fmt (rename_machine self v)
130
    | StateVar v    ->
131
      if Types.is_array_type v.var_type
132
      then assert false
133
      else pp_var fmt (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v))
134
    | Fun (n, vl)   -> Format.fprintf fmt "%a" (Basic_library.pp_horn n (pp_horn_val self pp_var)) vl
135
136
(* Prints a [value] indexed by the suffix list [loop_vars] *)
137
let rec pp_value_suffix self pp_value fmt value =
138
 match value with
139
 | Fun (n, vl)  ->
140
   Basic_library.pp_horn n (pp_value_suffix self pp_value) fmt vl
141
 |  _            ->
142
   pp_horn_val self pp_value fmt value
143
144
(* type_directed assignment: array vs. statically sized type
145
   - [var_type]: type of variable to be assigned
146
   - [var_name]: name of variable to be assigned
147
   - [value]: assigned value
148
   - [pp_var]: printer for variables
149
*)
150
let pp_assign m self pp_var fmt var_type var_name value =
151
  fprintf fmt "(= %a %a)" (pp_horn_val ~is_lhs:true self pp_var) var_name (pp_value_suffix self pp_var) value
152
153
let pp_instance_call
154
    machines ?(init=false) m self fmt i (inputs: value_t list) (outputs: var_decl list) =
155
  try (* stateful node instance *)
156
    begin
157
      let (n,_) = List.assoc i m.minstances in
158
      match node_name n, inputs, outputs with
159
      | "_arrow", [i1; i2], [o] -> begin
160
        if init then
161
          pp_assign
162
   	    m
163
   	    self
164
   	    (pp_horn_var m)
165
	    fmt
166
   	    o.var_type (LocalVar o) i1
167
        else
168
          pp_assign
169
   	    m self (pp_horn_var m) fmt
170
   	    o.var_type (LocalVar o) i2
171
172
      end
173
      | name, _, _ ->
174
	begin
175
	  let target_machine = List.find (fun m  -> m.mname.node_id = name) machines in
176
	  if init then
177
	    Format.fprintf fmt "(%a %a%t%a%t%a)"
178
	      pp_machine_init_name (node_name n)
179
	      (* inputs *)
180
	      (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m)))
181
	      inputs
182
	      (Utils.pp_final_char_if_non_empty " " inputs)
183
	      (* outputs *)
184
	      (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m)))
185
	      (List.map (fun v -> LocalVar v) outputs)
186
	      (Utils.pp_final_char_if_non_empty " " outputs)
187
	      (* memories (next) *)
188
	      (Utils.fprintf_list ~sep:" " pp_var) (
189
  		rename_machine_list
190
		  (concat m.mname.node_id i)
191
		  (rename_next_list (full_memory_vars machines target_machine)
192
		  )
193
	       )
194
	  else
195
	    Format.fprintf fmt "(%a %a%t%a%t%a)"
196
	      pp_machine_step_name (node_name n)
197
	      (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) inputs
198
	      (Utils.pp_final_char_if_non_empty " " inputs)
199
	      (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m)))
200
	      (List.map (fun v -> LocalVar v) outputs)
201
	      (Utils.pp_final_char_if_non_empty " " outputs)
202
	      (Utils.fprintf_list ~sep:" " pp_var) (
203
		(rename_machine_list
204
		   (concat m.mname.node_id i)
205
		   (rename_current_list (full_memory_vars machines target_machine))
206
		) @
207
		  (rename_machine_list
208
		     (concat m.mname.node_id i)
209
		     (rename_next_list (full_memory_vars machines target_machine))
210
		  )
211
	       )
212
213
	end
214
    end
215
    with Not_found -> ( (* stateless node instance *)
216
      let (n,_) = List.assoc i m.mcalls in
217
      Format.fprintf fmt "(%s %a%t%a)"
218
	(node_name n)
219
	(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m)))
220
	inputs
221
	(Utils.pp_final_char_if_non_empty " " inputs)
222
	(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m)))
223
	(List.map (fun v -> LocalVar v) outputs)
224
    )
225
226
let pp_machine_init (m: machine_t) self fmt inst =
227
  let (node, static) = List.assoc inst m.minstances in
228
  fprintf fmt "(%a %a%t%s->%s)"
229
    pp_machine_init_name (node_name node)
230
    (Utils.fprintf_list ~sep:" " Dimension.pp_dimension) static
231
    (Utils.pp_final_char_if_non_empty " " static)
232
    self inst
233
234 7c95dcab ploc
235
let rec pp_bool_conditional machines ?(init=false)  (m: machine_t) self fmt c tl el =
236 96d33ff2 tkahsai
  fprintf fmt "@[<v 2>if (%a) {%t%a@]@,@[<v 2>} else {%t%a@]@,}"
237
    (pp_horn_val self (pp_horn_var m)) c
238
    (Utils.pp_newline_if_non_empty tl)
239
    (Utils.fprintf_list ~sep:"@," (pp_machine_instr machines ~init:init  m self)) tl
240
    (Utils.pp_newline_if_non_empty el)
241
    (Utils.fprintf_list ~sep:"@," (pp_machine_instr machines ~init:init  m self)) el
242 7c95dcab ploc
(* and pp_enum_conditional machines ?(init=false)  (m: machine_t) self fmt g hl = *)
243
(* (\* TODO: check that the enum has all its constructor defined: Xavier how have you handled that, could we have partial definition? *\) *)
244
(*   match hl with *)
245
(*   | [] -> assert false *)
246
(*   | [el] -> Utils.fprintf_list ~sep:"@," (pp_machine_instr machines ~init:init  m self) fmt el *)
247
(*   | hd::tl -> *)
248
(*   fprintf fmt "@[<v 2>if (= %a %a) {%t%a@]@,@[<v 2>} else {@.(%a)xxxx@]@,}" *)
249
(*     (pp_horn_val self (pp_horn_var m)) c *)
250
(*     TODOg *)
251
(*     (Utils.pp_newline_if_non_empty tl) *)
252
(*     (Utils.fprintf_list ~sep:"@," (pp_machine_instr machines ~init:init  m self)) hd *)
253
(*     pp_print_newline fmt; *)
254
    
255
    
256
(* fprintf fmt  *)
257 96d33ff2 tkahsai
and pp_machine_instr machines ?(init=false) (m: machine_t) self fmt instr =
258
  match instr with
259
  | MReset i ->
260
    pp_machine_init m self fmt i
261
  | MLocalAssign (i,v) ->
262
    pp_assign
263
      m self (pp_horn_var m) fmt
264
      i.var_type (LocalVar i) v
265
  | MStateAssign (i,v) ->
266
    pp_assign
267
      m self (pp_horn_var m) fmt
268
      i.var_type (StateVar i) v
269
  | MStep ([i0], i, vl) when Basic_library.is_internal_fun i  ->
270
    assert false (* This should not happen anymore *)
271
  | MStep (il, i, vl) ->
272
    pp_instance_call machines ~init:init m self fmt i vl il
273 7c95dcab ploc
  | MBranch (g,hl) -> (* should not be produced *)
274
    assert false
275
276
    (* if hl <> [] && let t = fst (List.hd hl) in t = tag_true || t = tag_false *)
277
    (* then (\* boolean case, needs special treatment in C because truth value is not unique *\) *)
278
    (*   (\* may disappear if we optimize code by replacing last branch test with default *\) *)
279
    (*   let tl = try List.assoc tag_true  hl with Not_found -> [] in *)
280
    (*   let el = try List.assoc tag_false hl with Not_found -> [] in *)
281
    (*   pp_bool_conditional machines ~init:init m self fmt g tl el *)
282
    (* else (\* enum type case *\) *)
283
284
    (*   pp_enum_conditional machines ~init:init m self fmt g hl  *)
285 96d33ff2 tkahsai
286
287
(**************************************************************)
288
289
let is_stateless m = m.minstances = [] && m.mmemory = []
290
291
(* Print the machine m:
292
   two functions: m_init and m_step
293
   - m_init is a predicate over m memories
294
   - m_step is a predicate over old_memories, inputs, new_memories, outputs
295
   We first declare all variables then the two /rules/.
296
*)
297
let print_machine machines fmt m =
298
  let pp_instr init = pp_machine_instr machines ~init:init m in
299
  if m.mname.node_id = arrow_id then
300
    (* We don't print arrow function *)
301
    ()
302
  else
303
    begin
304
      Format.fprintf fmt "; %s@." m.mname.node_id;
305
306
   (* Printing variables *)
307
   Utils.fprintf_list ~sep:"@." pp_decl_var fmt
308
     ((step_vars machines m)@
309
	 (rename_machine_list m.mname.node_id m.mstep.step_locals));
310
   Format.pp_print_newline fmt ();
311
312
313
314
   if is_stateless m then
315
     begin
316
       (* Declaring single predicate *)
317
       Format.fprintf fmt "(declare-rel %a (%a))@."
318
	 pp_machine_stateless_name m.mname.node_id
319
	 (Utils.fprintf_list ~sep:" " pp_type)
320
	 (List.map (fun v -> v.var_type) (stateless_vars machines m));
321
322
       (* Rule for single predicate *)
323
       Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@."
324
	 (pp_conj (pp_instr
325
		     true (* In this case, the boolean init can be set to true or false.
326
			     The node is stateless. *)
327
		     m.mname.node_id)
328
	 )
329 7130028e ploc
	 m.mstep.step_instrs
330
	 pp_machine_stateless_name m.mname.node_id
331
	 (Utils.fprintf_list ~sep:" " pp_var) (stateless_vars machines m);
332
     end
333 3c862628 tkahsai
   else
334 7130028e ploc
     begin
335
       (* Declaring predicate *)
336
       Format.fprintf fmt "(declare-rel %a (%a))@."
337
	 pp_machine_init_name m.mname.node_id
338 3c862628 tkahsai
	 (Utils.fprintf_list ~sep:" " pp_type)
339 36454535 ploc
	 (List.map (fun v -> v.var_type) (init_vars machines m));
340 3c862628 tkahsai
341 7130028e ploc
       Format.fprintf fmt "(declare-rel %a (%a))@."
342
	 pp_machine_step_name m.mname.node_id
343 3c862628 tkahsai
	 (Utils.fprintf_list ~sep:" " pp_type)
344 36454535 ploc
	 (List.map (fun v -> v.var_type) (step_vars machines m));
345 3c862628 tkahsai
346 7130028e ploc
       Format.pp_print_newline fmt ();
347
348 36454535 ploc
       (* Rule for init *)
349 9c4624e4 tkahsai
       Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@."
350
	 (pp_conj (pp_instr true m.mname.node_id)) m.mstep.step_instrs
351
	 pp_machine_init_name m.mname.node_id
352
	 (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m);
353 ea94d58f tkahsai
354 62f65f02 tkahsai
      (* Adding assertions *)
355 36454535 ploc
       (match m.mstep.step_asserts with
356 ea94d58f tkahsai
       | [] ->
357
          begin
358 62f65f02 tkahsai
            (* Rule for init *)
359
            Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@."
360
	                   (pp_conj (pp_instr true m.mname.node_id)) m.mstep.step_instrs
361
	                   pp_machine_init_name m.mname.node_id
362
	                   (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m);
363
            (* Rule for step*)
364 ea94d58f tkahsai
            Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@."
365
                           (pp_conj (pp_instr false m.mname.node_id)) m.mstep.step_instrs
366
                           pp_machine_step_name m.mname.node_id
367
                           (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m);
368
          end
369
       | assertsl ->
370
          begin
371
	    let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id pp_var in
372
            (* print_string pp_val; *)
373
            let instrs_concat = m.mstep.step_instrs in
374 62f65f02 tkahsai
            Format.fprintf fmt "; with Assertions @.";
375
            (*Rule for init*)
376
            Format.fprintf fmt "@[<v 2>(rule (=> @ (and @ %a@. %a)(%a %a)@]@.))@.@."
377
                           (pp_conj (pp_instr true m.mname.node_id)) instrs_concat
378
                           (pp_conj pp_val) assertsl
379
                           pp_machine_init_name m.mname.node_id
380
                           (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m);
381
            (*Rule for step*)
382 f133f964 tkahsai
            Format.fprintf fmt "@[<v 2>(rule (=> @ (and @ %a@. %a)(%a %a)@]@.))@.@."
383 ea94d58f tkahsai
                           (pp_conj (pp_instr false m.mname.node_id)) instrs_concat
384 f133f964 tkahsai
                           (pp_conj pp_val) assertsl
385 ea94d58f tkahsai
                           pp_machine_step_name m.mname.node_id
386
                           (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m);
387
          end
388 36454535 ploc
       );
389 7130028e ploc
     end
390
    end
391 3a60ec17 ploc
392
393 aa6b7d46 ploc
394 36454535 ploc
let collecting_semantics machines fmt node machine =
395 3a60ec17 ploc
    Format.fprintf fmt "; Collecting semantics for node %s@.@." node;
396 faa5e5c5 ploc
    (* We print the types of the main node "memory tree" TODO: add the output *)
397 3a60ec17 ploc
    let main_output =
398
     rename_machine_list machine.mname.node_id machine.mstep.step_outputs
399
    in
400 3c862628 tkahsai
    let main_output_dummy =
401 9334747d ploc
     rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_outputs
402
    in
403 3c862628 tkahsai
    let main_memory_next =
404 3a60ec17 ploc
      (rename_next_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @
405
      main_output
406 faa5e5c5 ploc
    in
407 3c862628 tkahsai
    let main_memory_current =
408 3a60ec17 ploc
      (rename_current_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @
409 9334747d ploc
      main_output_dummy
410 faa5e5c5 ploc
    in
411 587cdc0d ploc
412
    (* Special case when the main node is stateless *)
413 3c862628 tkahsai
    let init_name, step_name =
414 587cdc0d ploc
      if is_stateless machine then
415
	pp_machine_stateless_name, pp_machine_stateless_name
416
      else
417
	pp_machine_init_name, pp_machine_step_name
418
    in
419 36454535 ploc
420 3a60ec17 ploc
    Format.fprintf fmt "(declare-rel MAIN (%a))@."
421 3c862628 tkahsai
      (Utils.fprintf_list ~sep:" " pp_type)
422 faa5e5c5 ploc
      (List.map (fun v -> v.var_type) main_memory_next);
423 3c862628 tkahsai
424 faa5e5c5 ploc
    Format.fprintf fmt "; Initial set@.";
425
    Format.fprintf fmt "(declare-rel INIT_STATE ())@.";
426
    Format.fprintf fmt "(rule INIT_STATE)@.";
427 7130028e ploc
    Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>INIT_STATE@ (@[<v 0>%a %a@])@]@ )@ (MAIN %a)@]@.))@.@."
428 587cdc0d ploc
      init_name node
429 faa5e5c5 ploc
      (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines machine)
430 3a60ec17 ploc
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_next ;
431 faa5e5c5 ploc
432
    Format.fprintf fmt "; Inductive def@.";
433 9334747d ploc
    (Utils.fprintf_list ~sep:" " (fun fmt v -> Format.fprintf fmt "%a@." pp_decl_var v)) fmt main_output_dummy;
434 3c862628 tkahsai
    Format.fprintf fmt
435 7130028e ploc
      "@[<v 2>(rule (=> @ (and @[<v 0>(MAIN %a)@ (@[<v 0>%a %a@])@]@ )@ (MAIN %a)@]@.))@.@."
436 faa5e5c5 ploc
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_current
437 587cdc0d ploc
      step_name node
438 faa5e5c5 ploc
      (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines machine)
439 3c862628 tkahsai
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_next
440 faa5e5c5 ploc
441 36454535 ploc
let check_prop machines fmt node machine =
442
  let main_output =
443
    rename_machine_list machine.mname.node_id machine.mstep.step_outputs
444
  in
445 3c862628 tkahsai
  let main_memory_next =
446 36454535 ploc
    (rename_next_list (full_memory_vars machines machine)) @ main_output
447
  in
448
  Format.fprintf fmt "; Property def@.";
449
  Format.fprintf fmt "(declare-rel ERR ())@.";
450
  Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (MAIN %a)@])@ ERR))@."
451
    (pp_conj pp_var) main_output
452
    (Utils.fprintf_list ~sep:" " pp_var) main_memory_next
453 3a60ec17 ploc
    ;
454 9c4624e4 tkahsai
   if !Options.horn_query then Format.fprintf fmt "(query ERR)@."
455 faa5e5c5 ploc
456 36454535 ploc
457
let cex_computation machines fmt node machine =
458
    Format.fprintf fmt "; CounterExample computation for node %s@.@." node;
459
    (* We print the types of the cex node "memory tree" TODO: add the output *)
460
    let cex_input =
461
     rename_machine_list machine.mname.node_id machine.mstep.step_inputs
462
    in
463 3c862628 tkahsai
    let cex_input_dummy =
464 36454535 ploc
     rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_inputs
465
    in
466
    let cex_output =
467
     rename_machine_list machine.mname.node_id machine.mstep.step_outputs
468
    in
469 3c862628 tkahsai
    let cex_output_dummy =
470 36454535 ploc
     rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_outputs
471
    in
472 3c862628 tkahsai
    let cex_memory_next =
473 36454535 ploc
      cex_input @ (rename_next_list (full_memory_vars machines machine)) @ cex_output
474
    in
475 3c862628 tkahsai
    let cex_memory_current =
476 36454535 ploc
      cex_input_dummy @ (rename_current_list (full_memory_vars machines machine)) @ cex_output_dummy
477
    in
478
479
    (* Special case when the cex node is stateless *)
480 3c862628 tkahsai
    let init_name, step_name =
481 36454535 ploc
      if is_stateless machine then
482
	pp_machine_stateless_name, pp_machine_stateless_name
483
      else
484
	pp_machine_init_name, pp_machine_step_name
485
    in
486
487
    Format.fprintf fmt "(declare-rel CEX (Int %a))@.@."
488 3c862628 tkahsai
      (Utils.fprintf_list ~sep:" " pp_type)
489 36454535 ploc
      (List.map (fun v -> v.var_type) cex_memory_next);
490 3c862628 tkahsai
491 36454535 ploc
    Format.fprintf fmt "; Initial set@.";
492
    Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>INIT_STATE@ (@[<v 0>%a %a@])@]@ )@ (CEX 0 %a)@]@.))@.@."
493
      init_name node
494
      (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines machine)
495
      (Utils.fprintf_list ~sep:" " pp_var) cex_memory_next ;
496
497
    Format.fprintf fmt "; Inductive def@.";
498
    (* Declare dummy inputs. Outputs should have been declared previously with collecting sem *)
499
    (Utils.fprintf_list ~sep:" " (fun fmt v -> Format.fprintf fmt "%a@." pp_decl_var v)) fmt cex_input_dummy;
500
    Format.fprintf fmt "(declare-var cexcpt Int)@.";
501 3c862628 tkahsai
    Format.fprintf fmt
502 36454535 ploc
      "@[<v 2>(rule (=> @ (and @[<v 0>(CEX cexcpt %a)@ (@[<v 0>%a %a@])@]@ )@ (CEX (+ 1 cexcpt) %a)@]@.))@.@."
503
      (Utils.fprintf_list ~sep:" " pp_var) cex_memory_current
504
      step_name node
505
      (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines machine)
506 3c862628 tkahsai
      (Utils.fprintf_list ~sep:" " pp_var) cex_memory_next
507 36454535 ploc
508
let get_cex machines fmt node machine =
509
    let cex_input =
510
     rename_machine_list machine.mname.node_id machine.mstep.step_inputs
511
    in
512
    let cex_output =
513
     rename_machine_list machine.mname.node_id machine.mstep.step_outputs
514
    in
515 3c862628 tkahsai
  let cex_memory_next =
516 36454535 ploc
    cex_input @ (rename_next_list (full_memory_vars machines machine)) @ cex_output
517
  in
518
  Format.fprintf fmt "; Property def@.";
519
  Format.fprintf fmt "(declare-rel CEXTRACE ())@.";
520
  Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (CEX cexcpt %a)@])@ CEXTRACE))@."
521
    (pp_conj pp_var) cex_output
522
    (Utils.fprintf_list ~sep:" " pp_var) cex_memory_next
523
    ;
524 62f65f02 tkahsai
  Format.fprintf fmt "(query CEXTRACE)@."
525 36454535 ploc
526
527 3c862628 tkahsai
let main_print machines fmt =
528
if !Options.main_node <> "" then
529 36454535 ploc
  begin
530
    let node = !Options.main_node in
531
    let machine = get_machine machines node in
532
533
534
    collecting_semantics machines fmt node machine;
535
    check_prop machines fmt node machine;
536 fcf1fd96 tkahsai
    if !Options.horn_cex then(
537
      cex_computation machines fmt node machine;
538
      get_cex machines fmt node machine)
539 faa5e5c5 ploc
end
540
541 7c95dcab ploc
let print_type_definitions fmt =
542
  let cpt_type = ref 0 in
543
  Hashtbl.iter (fun typ decl ->
544
		match typ with
545
		| Tydec_const var ->
546
		   (match decl.top_decl_desc with
547
		    | TypeDef tdef -> (
548
		      match tdef.tydef_desc with
549
		      | Tydec_enum tl ->
550
			incr cpt_type;
551
			fprintf fmt "(declare-datatypes () ((%s %a));@.@."
552
			  var
553
			  (Utils.fprintf_list ~sep:" " pp_print_string) tl
554
		      | _ -> assert false
555
		    )
556
		    | _ -> assert false
557
		   )
558
		| _        -> ()) type_table
559
560 aa6b7d46 ploc
561
let translate fmt basename prog machines =
562 7c95dcab ploc
  (* We print typedef *)
563
  print_type_definitions fmt;
564
565 04a7df69 ploc
  List.iter (print_machine machines fmt) (List.rev machines);
566 3c862628 tkahsai
  main_print machines fmt
567 aa6b7d46 ploc
568
569 36454535 ploc
let traces_file fmt basename prog machines =
570 720f159a tkahsai
571 3c862628 tkahsai
  Format.fprintf fmt
572 720f159a tkahsai
  "<?xml version=\"1.0\"?>\n<Traces xmlns:xsi=\"http://www.w3.org/2001/XMLSchema-instance\">\n";
573 36454535 ploc
574
  (* We extract the annotation dealing with traceability *)
575 3c862628 tkahsai
  let machines_traces = List.map (fun m ->
576
    let traces : (ident * expr) list=
577 36454535 ploc
      let all_annots = List.flatten (List.map (fun ann -> ann.annots) m.mannot) in
578 3c862628 tkahsai
      let filtered =
579 e9c64a30 ploc
	List.filter (fun (kwds, _) -> kwds = ["traceability"]) all_annots
580 36454535 ploc
      in
581
      let content = List.map snd filtered in
582
      (* Elements are supposed to be a pair (tuple): variable, expression *)
583 3c862628 tkahsai
      List.map (fun ee ->
584
	match ee.eexpr_quantifiers, ee.eexpr_qfexpr.expr_desc with
585 36454535 ploc
	| [], Expr_tuple [v;e] -> (
586 3c862628 tkahsai
	  match v.expr_desc with
587
	  | Expr_ident vid -> vid, e
588 36454535 ploc
	  | _ -> assert false )
589
	| _ -> assert false)
590
	content
591
    in
592 3c862628 tkahsai
593 36454535 ploc
    m, traces
594
595
  ) machines
596
  in
597
598
  (* Compute memories associated to each machine *)
599
  let compute_mems m =
600
    let rec aux fst prefix m =
601
      (List.map (fun mem -> (prefix, mem)) m.mmemory) @
602 3c862628 tkahsai
	List.fold_left (fun accu (id, (n, _)) ->
603
	  let name = node_name n in
604 36454535 ploc
	  if name = "_arrow" then accu else
605
	    let machine_n = get_machine machines name in
606 3c862628 tkahsai
	    ( aux false ((id,machine_n)::prefix) machine_n )
607 36454535 ploc
	    @ accu
608 3c862628 tkahsai
	) [] m.minstances
609 36454535 ploc
    in
610
    aux true [] m
611
  in
612
613
  List.iter (fun m ->
614 720f159a tkahsai
    (* Format.fprintf fmt "; Node %s@." m.mname.node_id; *)
615
    Format.fprintf fmt "    <Node name=\"%s\">@." m.mname.node_id;
616 3c862628 tkahsai
617
    let memories_old =
618
      List.map (fun (p, v) ->
619 36454535 ploc
	let machine = match p with | [] -> m | (_,m')::_ -> m' in
620
	let traces = List.assoc machine machines_traces in
621 e9c64a30 ploc
	if List.mem_assoc v.var_id traces then (
622 36454535 ploc
	  (* We take the expression associated to variable v in the trace info *)
623 e9c64a30 ploc
	  (* Format.eprintf "Found variable %a in traces: %a@."  pp_var v Printers.pp_expr (List.assoc v.var_id traces); *)
624 36454535 ploc
	  p, List.assoc v.var_id traces
625 e9c64a30 ploc
      )
626
	else (
627 36454535 ploc
	  (* We keep the variable as is: we create an expression v *)
628 e9c64a30 ploc
	  (* 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); *)
629 36454535 ploc
	  p, mkexpr Location.dummy_loc (Expr_ident v.var_id)
630 e9c64a30 ploc
	)
631 3c862628 tkahsai
632
      ) (compute_mems m)
633 36454535 ploc
    in
634
    let memories_next = (* We remove the topest pre in each expression *)
635 3c862628 tkahsai
      List.map
636 e9c64a30 ploc
      	(fun (prefix, ee) ->
637
      	  match ee.expr_desc with
638
      	  | Expr_pre e -> prefix, e
639
      	  | _ -> Format.eprintf
640
      	    "Mem Failure: (prefix: %a, eexpr: %a)@.@?"
641
      	    (Utils.fprintf_list ~sep:","
642
      	       (fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id ))
643
      	    (List.rev prefix)
644
      	    Printers.pp_expr ee;
645
      	    assert false)
646 36454535 ploc
	memories_old
647
    in
648
649 9c4624e4 tkahsai
    (* let pp_prefix_rev fmt prefix = *)
650
    (*   Utils.fprintf_list ~sep:"." (fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id) fmt (List.rev prefix) *)
651
    (* in *)
652 36454535 ploc
653 9c4624e4 tkahsai
    let pp_prefix_rev fmt prefix =
654 933ee7a3 tkahsai
      Utils.fprintf_list ~sep:"." (fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id) fmt (List.rev prefix)
655
    in
656 9d01f989 ploc
657 933ee7a3 tkahsai
    let input_vars = (rename_machine_list m.mname.node_id m.mstep.step_inputs) in
658
    let output_vars = (rename_machine_list m.mname.node_id m.mstep.step_outputs) in
659
     Format.fprintf fmt "     <input name=\"%a\" type=\"%a\">%a</input> @."
660 9d01f989 ploc
                   (Utils.fprintf_list ~sep:" | " pp_var) input_vars
661 933ee7a3 tkahsai
                   (Utils.fprintf_list ~sep:" | "  (fun fmt id -> pp_type fmt id.var_type)) input_vars
662 720f159a tkahsai
                   (Utils.fprintf_list ~sep:" | " pp_var) (m.mstep.step_inputs);
663
664 933ee7a3 tkahsai
    Format.fprintf fmt "      <output name=\"%a\" type=\"%a\">%a</output> @."
665
                   (Utils.fprintf_list ~sep:" | " pp_var)  output_vars
666
                   (Utils.fprintf_list ~sep:" | "  (fun fmt id -> pp_type fmt id.var_type)) output_vars
667 720f159a tkahsai
                   (Utils.fprintf_list ~sep:" | " pp_var) (m.mstep.step_outputs);
668
669 933ee7a3 tkahsai
    let init_local_vars = (rename_next_list (full_memory_vars machines m)) in
670
    let step_local_vars = (rename_current_list (full_memory_vars machines m)) in
671 3c862628 tkahsai
672 933ee7a3 tkahsai
    Format.fprintf fmt "      <localInit name=\"%a\" type=\"%a\">%t%a</localInit> @."
673
                   (Utils.fprintf_list ~sep:" | " pp_var) init_local_vars
674
                   (Utils.fprintf_list ~sep:" | "  (fun fmt id -> pp_type fmt id.var_type)) init_local_vars
675
                   (fun fmt -> match memories_next with [] -> () | _ -> fprintf fmt "")
676
                   (Utils.fprintf_list ~sep:" | " (fun fmt (prefix, ee) -> fprintf fmt "%a" Printers.pp_expr ee)) memories_next;
677 720f159a tkahsai
678 933ee7a3 tkahsai
    Format.fprintf fmt "      <localStep name=\"%a\" type=\"%a\">%t%a</localStep> @."
679
                   (Utils.fprintf_list ~sep:" | " pp_var) step_local_vars
680
                   (Utils.fprintf_list ~sep:" | "  (fun fmt id -> pp_type fmt id.var_type)) step_local_vars
681
                   (fun fmt -> match memories_old with [] -> () | _ -> fprintf fmt "")
682
                     (Utils.fprintf_list ~sep:" | " (fun fmt (prefix,ee) -> fprintf fmt "(%a)"
683
                                    Printers.pp_expr ee)) (memories_old);
684 720f159a tkahsai
685
     Format.fprintf fmt "    </Node>@.";
686
687
  ) (List.rev machines);
688
  Format.fprintf fmt "</Traces>@.";
689 36454535 ploc
690 9c4624e4 tkahsai
          (* (Utils.fprintf_list ~sep:" | " (fun fmt (prefix, ee) -> fprintf fmt "%a%a" pp_prefix_rev prefix Printers.pp_expr ee)) memories_next; *)
691
   (* (Utils.fprintf_list ~sep:" | " (fun fmt (prefix,ee) -> fprintf fmt "%a(%a)" *)
692
   (*                                  pp_prefix_rev prefix Printers.pp_expr ee)) (memories_old); *)
693
694 aa6b7d46 ploc
(* Local Variables: *)
695 e9c64a30 ploc
(* compile-command:"make -C ../.." *)
696 aa6b7d46 ploc
(* End: *)