Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / backends / Horn / horn_backend.ml @ 99d9ac94

History | View | Annotate | Download (24.3 KB)

1 a2d97a3e ploc
(********************************************************************)
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 dcbf9d3a ploc
open Format
16
open LustreSpec
17
open Corelang
18
open Machine_code
19
20
21 f19eb2fd ploc
let pp_machine_init_name fmt id = fprintf fmt "%s_init" id
22 7a19992d ploc
let pp_machine_step_name fmt id = fprintf fmt "%s_step" id
23 bd3ef34a ploc
let pp_machine_stateless_name fmt id = fprintf fmt "%s" id
24 7a19992d ploc
25 dcbf9d3a ploc
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 cd6efd9b ploc
  | Types.Treal           -> Format.fprintf fmt "Real"
30 dcbf9d3a ploc
  | Types.Tclock _
31
  | Types.Tarray _
32
  | Types.Tstatic _
33
  | Types.Tconst _
34
  | Types.Tarrow _
35 5cf953ec tkahsai
  | _                     -> Format.eprintf "internal error: pp_type %a@."
36 a2d97a3e ploc
    Types.print_ty t; assert false
37 dcbf9d3a ploc
38 5cf953ec tkahsai
let pp_decl_var fmt id =
39 f19eb2fd ploc
  Format.fprintf fmt "(declare-var %s %a)"
40 dcbf9d3a ploc
    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 5cf953ec tkahsai
let pp_conj pp fmt l =
47
  match l with
48 af5af1e8 ploc
    [] -> assert false
49
  | [x] -> pp fmt x
50
  | _ -> fprintf fmt "(and @[<v 0>%a@]@ )" (Utils.fprintf_list ~sep:" " pp) l
51
52
53 5cf953ec tkahsai
54
let concat prefix x = if prefix = "" then x else prefix ^ "." ^ x
55 2f44a4cc ploc
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 c76f1d66 ploc
let rename_machine_list p = List.map (rename_machine p)
58 5cf953ec tkahsai
59 c76f1d66 ploc
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 20e9de2d ploc
65 5cf953ec tkahsai
let get_machine machines node_name =
66
  List.find (fun m  -> m.mname.node_id = node_name) machines
67 20e9de2d ploc
68 c7c6ef4c tkahsai
69 c76f1d66 ploc
let full_memory_vars machines machine =
70 2f44a4cc ploc
  let rec aux fst prefix m =
71
    (rename_machine_list (if fst then prefix else concat prefix m.mname.node_id) m.mmemory) @
72 5cf953ec tkahsai
      List.fold_left (fun accu (id, (n, _)) ->
73
	let name = node_name n in
74 20e9de2d ploc
	if name = "_arrow" then accu else
75
	  let machine_n = get_machine machines name in
76 a2d97a3e ploc
	  ( aux false (concat prefix (if fst then id else concat m.mname.node_id id)) machine_n ) @ accu
77 5cf953ec tkahsai
      ) [] (m.minstances)
78 20e9de2d ploc
  in
79 c76f1d66 ploc
  aux true machine.mname.node_id machine
80 20e9de2d ploc
81 c7c6ef4c tkahsai
82 5cf953ec tkahsai
let stateless_vars machines m =
83 bd3ef34a ploc
  (rename_machine_list m.mname.node_id m.mstep.step_inputs)@
84
    (rename_machine_list m.mname.node_id m.mstep.step_outputs)
85 5cf953ec tkahsai
86
let step_vars machines m =
87 bd3ef34a ploc
  (stateless_vars machines m)@
88 5cf953ec tkahsai
    (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 7a19992d ploc
(********************************************************************************************)
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 2f44a4cc ploc
  pp_print_string fmt (if t = tag_true then "true" else if t = tag_false then "false" else t)
109 7a19992d ploc
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 12af4908 xthirioux
    | _              -> assert false
118 7a19992d ploc
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 5cf953ec tkahsai
    | Array _
127 7a19992d ploc
    | 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 5cf953ec tkahsai
      then assert false
133 2f44a4cc ploc
      else pp_var fmt (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v))
134 c76f1d66 ploc
    | Fun (n, vl)   -> Format.fprintf fmt "%a" (Basic_library.pp_horn n (pp_horn_val self pp_var)) vl
135 7a19992d ploc
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 96babff4 ploc
  fprintf fmt "(= %a %a)" (pp_horn_val ~is_lhs:true self pp_var) var_name (pp_value_suffix self pp_var) value
152 5cf953ec tkahsai
153
let pp_instance_call
154 8605c4a4 ploc
    machines ?(init=false) m self fmt i (inputs: value_t list) (outputs: var_decl list) =
155 5cf953ec tkahsai
  try (* stateful node instance *)
156 8605c4a4 ploc
    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 af5af1e8 ploc
        if init then
161
          pp_assign
162
   	    m
163
   	    self
164 5cf953ec tkahsai
   	    (pp_horn_var m)
165 af5af1e8 ploc
	    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 5cf953ec tkahsai
172 8605c4a4 ploc
      end
173 5cf953ec tkahsai
      | name, _, _ ->
174 8605c4a4 ploc
	begin
175
	  let target_machine = List.find (fun m  -> m.mname.node_id = name) machines in
176 20e9de2d ploc
	  if init then
177 af5af1e8 ploc
	    Format.fprintf fmt "(%a %a%t%a%t%a)"
178 5cf953ec tkahsai
	      pp_machine_init_name (node_name n)
179 af5af1e8 ploc
	      (* inputs *)
180 5cf953ec tkahsai
	      (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m)))
181 af5af1e8 ploc
	      inputs
182 5cf953ec tkahsai
	      (Utils.pp_final_char_if_non_empty " " inputs)
183 af5af1e8 ploc
	      (* outputs *)
184 5cf953ec tkahsai
	      (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m)))
185 af5af1e8 ploc
	      (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 5cf953ec tkahsai
  		rename_machine_list
190
		  (concat m.mname.node_id i)
191 af5af1e8 ploc
		  (rename_next_list (full_memory_vars machines target_machine)
192 5cf953ec tkahsai
		  )
193 af5af1e8 ploc
	       )
194 20e9de2d ploc
	  else
195 bd3ef34a ploc
	    Format.fprintf fmt "(%a %a%t%a%t%a)"
196 5cf953ec tkahsai
	      pp_machine_step_name (node_name n)
197 20e9de2d ploc
	      (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) inputs
198 5cf953ec tkahsai
	      (Utils.pp_final_char_if_non_empty " " inputs)
199
	      (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m)))
200 af5af1e8 ploc
	      (List.map (fun v -> LocalVar v) outputs)
201 20e9de2d ploc
	      (Utils.pp_final_char_if_non_empty " " outputs)
202
	      (Utils.fprintf_list ~sep:" " pp_var) (
203 5cf953ec tkahsai
		(rename_machine_list
204
		   (concat m.mname.node_id i)
205 af5af1e8 ploc
		   (rename_current_list (full_memory_vars machines target_machine))
206 5cf953ec tkahsai
		) @
207
		  (rename_machine_list
208
		     (concat m.mname.node_id i)
209 af5af1e8 ploc
		     (rename_next_list (full_memory_vars machines target_machine))
210 5cf953ec tkahsai
		  )
211 20e9de2d ploc
	       )
212 5cf953ec tkahsai
213 bd3ef34a ploc
	end
214 8605c4a4 ploc
    end
215
    with Not_found -> ( (* stateless node instance *)
216
      let (n,_) = List.assoc i m.mcalls in
217 bd3ef34a ploc
      Format.fprintf fmt "(%s %a%t%a)"
218
	(node_name n)
219 5cf953ec tkahsai
	(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m)))
220 af5af1e8 ploc
	inputs
221 5cf953ec tkahsai
	(Utils.pp_final_char_if_non_empty " " inputs)
222
	(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m)))
223 af5af1e8 ploc
	(List.map (fun v -> LocalVar v) outputs)
224 8605c4a4 ploc
    )
225 7a19992d ploc
226 f19eb2fd ploc
let pp_machine_init (m: machine_t) self fmt inst =
227 7a19992d ploc
  let (node, static) = List.assoc inst m.minstances in
228
  fprintf fmt "(%a %a%t%s->%s)"
229 f19eb2fd ploc
    pp_machine_init_name (node_name node)
230 7a19992d ploc
    (Utils.fprintf_list ~sep:" " Dimension.pp_dimension) static
231
    (Utils.pp_final_char_if_non_empty " " static)
232
    self inst
233
234
(* TODO *)
235
let rec pp_conditional machines ?(init=false)  (m: machine_t) self fmt c tl el =
236
  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
243
and pp_machine_instr machines ?(init=false) (m: machine_t) self fmt instr =
244 5cf953ec tkahsai
  match instr with
245 7a19992d ploc
  | MReset i ->
246 f19eb2fd ploc
    pp_machine_init m self fmt i
247 7a19992d ploc
  | MLocalAssign (i,v) ->
248
    pp_assign
249
      m self (pp_horn_var m) fmt
250
      i.var_type (LocalVar i) v
251
  | MStateAssign (i,v) ->
252
    pp_assign
253
      m self (pp_horn_var m) fmt
254
      i.var_type (StateVar i) v
255 5cf953ec tkahsai
  | MStep ([i0], i, vl) when Basic_library.is_internal_fun i  ->
256 af5af1e8 ploc
    assert false (* This should not happen anymore *)
257 7a19992d ploc
  | MStep (il, i, vl) ->
258
    pp_instance_call machines ~init:init m self fmt i vl il
259
  | MBranch (g,hl) ->
260
    if hl <> [] && let t = fst (List.hd hl) in t = tag_true || t = tag_false
261
    then (* boolean case, needs special treatment in C because truth value is not unique *)
262 af5af1e8 ploc
      (* may disappear if we optimize code by replacing last branch test with default *)
263 7a19992d ploc
      let tl = try List.assoc tag_true  hl with Not_found -> [] in
264
      let el = try List.assoc tag_false hl with Not_found -> [] in
265
      pp_conditional machines ~init:init m self fmt g tl el
266
    else assert false (* enum type case *)
267
268
269
(**************************************************************)
270 4162f7a0 ploc
271 5cf953ec tkahsai
let is_stateless m = m.minstances = [] && m.mmemory = []
272
273
(* Print the machine m:
274 dcbf9d3a ploc
   two functions: m_init and m_step
275
   - m_init is a predicate over m memories
276
   - m_step is a predicate over old_memories, inputs, new_memories, outputs
277
   We first declare all variables then the two /rules/.
278
*)
279 5cf953ec tkahsai
let print_machine machines fmt m =
280 7a19992d ploc
  let pp_instr init = pp_machine_instr machines ~init:init m in
281 5cf953ec tkahsai
  if m.mname.node_id = arrow_id then
282 bd3ef34a ploc
    (* We don't print arrow function *)
283
    ()
284 5cf953ec tkahsai
  else
285
    begin
286 bd3ef34a ploc
      Format.fprintf fmt "; %s@." m.mname.node_id;
287
288 dcbf9d3a ploc
   (* Printing variables *)
289 5cf953ec tkahsai
   Utils.fprintf_list ~sep:"@." pp_decl_var fmt
290 bd3ef34a ploc
     ((step_vars machines m)@
291
	 (rename_machine_list m.mname.node_id m.mstep.step_locals));
292 7a19992d ploc
   Format.pp_print_newline fmt ();
293 dcbf9d3a ploc
294 5cf953ec tkahsai
295
296 4162f7a0 ploc
   if is_stateless m then
297 bd3ef34a ploc
     begin
298
       (* Declaring single predicate *)
299
       Format.fprintf fmt "(declare-rel %a (%a))@."
300
	 pp_machine_stateless_name m.mname.node_id
301 5cf953ec tkahsai
	 (Utils.fprintf_list ~sep:" " pp_type)
302 bd3ef34a ploc
	 (List.map (fun v -> v.var_type) (stateless_vars machines m));
303 5cf953ec tkahsai
304 bd3ef34a ploc
       (* Rule for single predicate *)
305 af5af1e8 ploc
       Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@."
306 5cf953ec tkahsai
	 (pp_conj (pp_instr
307
		     true (* In this case, the boolean init can be set to true or false.
308 af5af1e8 ploc
			     The node is stateless. *)
309
		     m.mname.node_id)
310
	 )
311 bd3ef34a ploc
	 m.mstep.step_instrs
312
	 pp_machine_stateless_name m.mname.node_id
313
	 (Utils.fprintf_list ~sep:" " pp_var) (stateless_vars machines m);
314
     end
315 5cf953ec tkahsai
   else
316 bd3ef34a ploc
     begin
317
       (* Declaring predicate *)
318
       Format.fprintf fmt "(declare-rel %a (%a))@."
319
	 pp_machine_init_name m.mname.node_id
320 5cf953ec tkahsai
	 (Utils.fprintf_list ~sep:" " pp_type)
321 af5af1e8 ploc
	 (List.map (fun v -> v.var_type) (init_vars machines m));
322 5cf953ec tkahsai
323 bd3ef34a ploc
       Format.fprintf fmt "(declare-rel %a (%a))@."
324
	 pp_machine_step_name m.mname.node_id
325 5cf953ec tkahsai
	 (Utils.fprintf_list ~sep:" " pp_type)
326 af5af1e8 ploc
	 (List.map (fun v -> v.var_type) (step_vars machines m));
327 5cf953ec tkahsai
328 bd3ef34a ploc
       Format.pp_print_newline fmt ();
329
330 af5af1e8 ploc
       (* Rule for init *)
331 99d9ac94 tkahsai
       (* Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@." *)
332
       (*   (pp_conj (pp_instr true m.mname.node_id)) m.mstep.step_instrs *)
333
       (*   pp_machine_init_name m.mname.node_id *)
334
       (*   (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m); *)
335 bd3ef34a ploc
336 8d4fddd8 tkahsai
       (* (\* Rule for step *\) *)
337
       (* Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@." *)
338
       (*   (pp_conj (pp_instr false m.mname.node_id)) m.mstep.step_instrs *)
339
       (*   pp_machine_step_name m.mname.node_id *)
340
       (*   (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m); *)
341 af5af1e8 ploc
342 8d4fddd8 tkahsai
343 c7c6ef4c tkahsai
      (* Adding assertions *)
344 af5af1e8 ploc
       (match m.mstep.step_asserts with
345 8d4fddd8 tkahsai
       | [] ->
346
          begin
347 c7c6ef4c tkahsai
            (* Rule for init *)
348
            Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@."
349
	                   (pp_conj (pp_instr true m.mname.node_id)) m.mstep.step_instrs
350
	                   pp_machine_init_name m.mname.node_id
351
	                   (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m);
352
            (* Rule for step*)
353 8d4fddd8 tkahsai
            Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@."
354
                           (pp_conj (pp_instr false m.mname.node_id)) m.mstep.step_instrs
355
                           pp_machine_step_name m.mname.node_id
356
                           (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m);
357
          end
358
       | assertsl ->
359
          begin
360
	    let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id pp_var in
361
            (* print_string pp_val; *)
362
            let instrs_concat = m.mstep.step_instrs in
363 c7c6ef4c tkahsai
            Format.fprintf fmt "; with Assertions @.";
364
            (*Rule for init*)
365
            Format.fprintf fmt "@[<v 2>(rule (=> @ (and @ %a@. %a)(%a %a)@]@.))@.@."
366
                           (pp_conj (pp_instr true m.mname.node_id)) instrs_concat
367
                           (pp_conj pp_val) assertsl
368
                           pp_machine_init_name m.mname.node_id
369
                           (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m);
370
            (*Rule for step*)
371 7d9df109 tkahsai
            Format.fprintf fmt "@[<v 2>(rule (=> @ (and @ %a@. %a)(%a %a)@]@.))@.@."
372 8d4fddd8 tkahsai
                           (pp_conj (pp_instr false m.mname.node_id)) instrs_concat
373 7d9df109 tkahsai
                           (pp_conj pp_val) assertsl
374 8d4fddd8 tkahsai
                           pp_machine_step_name m.mname.node_id
375
                           (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m);
376 7d9df109 tkahsai
	    (* Format.fprintf fmt " @[<v 2>%a@]@ @.@.@." *)
377
            (*                 (pp_conj pp_val) assertsl; *)
378
379 8d4fddd8 tkahsai
          end
380 af5af1e8 ploc
       );
381 5cf953ec tkahsai
382
383 bd3ef34a ploc
     end
384
    end
385 9cab57c9 ploc
386
387 dcbf9d3a ploc
388 af5af1e8 ploc
let collecting_semantics machines fmt node machine =
389 9cab57c9 ploc
    Format.fprintf fmt "; Collecting semantics for node %s@.@." node;
390 20e9de2d ploc
    (* We print the types of the main node "memory tree" TODO: add the output *)
391 9cab57c9 ploc
    let main_output =
392
     rename_machine_list machine.mname.node_id machine.mstep.step_outputs
393
    in
394 5cf953ec tkahsai
    let main_output_dummy =
395 4be0d54a ploc
     rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_outputs
396
    in
397 5cf953ec tkahsai
    let main_memory_next =
398 9cab57c9 ploc
      (rename_next_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @
399
      main_output
400 20e9de2d ploc
    in
401 5cf953ec tkahsai
    let main_memory_current =
402 9cab57c9 ploc
      (rename_current_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @
403 4be0d54a ploc
      main_output_dummy
404 20e9de2d ploc
    in
405 4162f7a0 ploc
406
    (* Special case when the main node is stateless *)
407 5cf953ec tkahsai
    let init_name, step_name =
408 4162f7a0 ploc
      if is_stateless machine then
409
	pp_machine_stateless_name, pp_machine_stateless_name
410
      else
411
	pp_machine_init_name, pp_machine_step_name
412
    in
413 af5af1e8 ploc
414 9cab57c9 ploc
    Format.fprintf fmt "(declare-rel MAIN (%a))@."
415 5cf953ec tkahsai
      (Utils.fprintf_list ~sep:" " pp_type)
416 20e9de2d ploc
      (List.map (fun v -> v.var_type) main_memory_next);
417 5cf953ec tkahsai
418 20e9de2d ploc
    Format.fprintf fmt "; Initial set@.";
419
    Format.fprintf fmt "(declare-rel INIT_STATE ())@.";
420
    Format.fprintf fmt "(rule INIT_STATE)@.";
421 bd3ef34a ploc
    Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>INIT_STATE@ (@[<v 0>%a %a@])@]@ )@ (MAIN %a)@]@.))@.@."
422 4162f7a0 ploc
      init_name node
423 20e9de2d ploc
      (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines machine)
424 9cab57c9 ploc
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_next ;
425 20e9de2d ploc
426
    Format.fprintf fmt "; Inductive def@.";
427 4be0d54a ploc
    (Utils.fprintf_list ~sep:" " (fun fmt v -> Format.fprintf fmt "%a@." pp_decl_var v)) fmt main_output_dummy;
428 5cf953ec tkahsai
    Format.fprintf fmt
429 bd3ef34a ploc
      "@[<v 2>(rule (=> @ (and @[<v 0>(MAIN %a)@ (@[<v 0>%a %a@])@]@ )@ (MAIN %a)@]@.))@.@."
430 20e9de2d ploc
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_current
431 4162f7a0 ploc
      step_name node
432 20e9de2d ploc
      (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines machine)
433 5cf953ec tkahsai
      (Utils.fprintf_list ~sep:" " pp_var) main_memory_next
434 20e9de2d ploc
435 af5af1e8 ploc
let check_prop machines fmt node machine =
436
  let main_output =
437
    rename_machine_list machine.mname.node_id machine.mstep.step_outputs
438
  in
439 5cf953ec tkahsai
  let main_memory_next =
440 af5af1e8 ploc
    (rename_next_list (full_memory_vars machines machine)) @ main_output
441
  in
442
  Format.fprintf fmt "; Property def@.";
443
  Format.fprintf fmt "(declare-rel ERR ())@.";
444
  Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (MAIN %a)@])@ ERR))@."
445
    (pp_conj pp_var) main_output
446
    (Utils.fprintf_list ~sep:" " pp_var) main_memory_next
447 9cab57c9 ploc
    ;
448 c7c6ef4c tkahsai
   Format.fprintf fmt "(query ERR)@."
449 20e9de2d ploc
450 af5af1e8 ploc
451
let cex_computation machines fmt node machine =
452
    Format.fprintf fmt "; CounterExample computation for node %s@.@." node;
453
    (* We print the types of the cex node "memory tree" TODO: add the output *)
454
    let cex_input =
455
     rename_machine_list machine.mname.node_id machine.mstep.step_inputs
456
    in
457 5cf953ec tkahsai
    let cex_input_dummy =
458 af5af1e8 ploc
     rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_inputs
459
    in
460
    let cex_output =
461
     rename_machine_list machine.mname.node_id machine.mstep.step_outputs
462
    in
463 5cf953ec tkahsai
    let cex_output_dummy =
464 af5af1e8 ploc
     rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_outputs
465
    in
466 5cf953ec tkahsai
    let cex_memory_next =
467 af5af1e8 ploc
      cex_input @ (rename_next_list (full_memory_vars machines machine)) @ cex_output
468
    in
469 5cf953ec tkahsai
    let cex_memory_current =
470 af5af1e8 ploc
      cex_input_dummy @ (rename_current_list (full_memory_vars machines machine)) @ cex_output_dummy
471
    in
472
473
    (* Special case when the cex node is stateless *)
474 5cf953ec tkahsai
    let init_name, step_name =
475 af5af1e8 ploc
      if is_stateless machine then
476
	pp_machine_stateless_name, pp_machine_stateless_name
477
      else
478
	pp_machine_init_name, pp_machine_step_name
479
    in
480
481
    Format.fprintf fmt "(declare-rel CEX (Int %a))@.@."
482 5cf953ec tkahsai
      (Utils.fprintf_list ~sep:" " pp_type)
483 af5af1e8 ploc
      (List.map (fun v -> v.var_type) cex_memory_next);
484 5cf953ec tkahsai
485 af5af1e8 ploc
    Format.fprintf fmt "; Initial set@.";
486
    Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>INIT_STATE@ (@[<v 0>%a %a@])@]@ )@ (CEX 0 %a)@]@.))@.@."
487
      init_name node
488
      (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines machine)
489
      (Utils.fprintf_list ~sep:" " pp_var) cex_memory_next ;
490
491
    Format.fprintf fmt "; Inductive def@.";
492
    (* Declare dummy inputs. Outputs should have been declared previously with collecting sem *)
493
    (Utils.fprintf_list ~sep:" " (fun fmt v -> Format.fprintf fmt "%a@." pp_decl_var v)) fmt cex_input_dummy;
494
    Format.fprintf fmt "(declare-var cexcpt Int)@.";
495 5cf953ec tkahsai
    Format.fprintf fmt
496 af5af1e8 ploc
      "@[<v 2>(rule (=> @ (and @[<v 0>(CEX cexcpt %a)@ (@[<v 0>%a %a@])@]@ )@ (CEX (+ 1 cexcpt) %a)@]@.))@.@."
497
      (Utils.fprintf_list ~sep:" " pp_var) cex_memory_current
498
      step_name node
499
      (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines machine)
500 5cf953ec tkahsai
      (Utils.fprintf_list ~sep:" " pp_var) cex_memory_next
501 af5af1e8 ploc
502
let get_cex machines fmt node machine =
503
    let cex_input =
504
     rename_machine_list machine.mname.node_id machine.mstep.step_inputs
505
    in
506
    let cex_output =
507
     rename_machine_list machine.mname.node_id machine.mstep.step_outputs
508
    in
509 5cf953ec tkahsai
  let cex_memory_next =
510 af5af1e8 ploc
    cex_input @ (rename_next_list (full_memory_vars machines machine)) @ cex_output
511
  in
512
  Format.fprintf fmt "; Property def@.";
513
  Format.fprintf fmt "(declare-rel CEXTRACE ())@.";
514
  Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (CEX cexcpt %a)@])@ CEXTRACE))@."
515
    (pp_conj pp_var) cex_output
516
    (Utils.fprintf_list ~sep:" " pp_var) cex_memory_next
517
    ;
518 c7c6ef4c tkahsai
  Format.fprintf fmt "(query CEXTRACE)@."
519 af5af1e8 ploc
520
521 5cf953ec tkahsai
let main_print machines fmt =
522
if !Options.main_node <> "" then
523 af5af1e8 ploc
  begin
524
    let node = !Options.main_node in
525
    let machine = get_machine machines node in
526
527
528
    collecting_semantics machines fmt node machine;
529
    check_prop machines fmt node machine;
530 43aa67ec tkahsai
    if !Options.horn_cex then(
531
      cex_computation machines fmt node machine;
532
      get_cex machines fmt node machine)
533 20e9de2d ploc
end
534
535 dcbf9d3a ploc
536
let translate fmt basename prog machines =
537 7a19992d ploc
  List.iter (print_machine machines fmt) (List.rev machines);
538 5cf953ec tkahsai
  main_print machines fmt
539 dcbf9d3a ploc
540
541 af5af1e8 ploc
let traces_file fmt basename prog machines =
542 5cf953ec tkahsai
  Format.fprintf fmt
543 af5af1e8 ploc
    "; Horn code traceability generated by %s@.; SVN version number %s@.@."
544 5cf953ec tkahsai
    (Filename.basename Sys.executable_name)
545 af5af1e8 ploc
    Version.number;
546
547
  (* We extract the annotation dealing with traceability *)
548 5cf953ec tkahsai
  let machines_traces = List.map (fun m ->
549
    let traces : (ident * expr) list=
550 af5af1e8 ploc
      let all_annots = List.flatten (List.map (fun ann -> ann.annots) m.mannot) in
551 5cf953ec tkahsai
      let filtered =
552 3ca6d126 ploc
	List.filter (fun (kwds, _) -> kwds = ["traceability"]) all_annots
553 af5af1e8 ploc
      in
554
      let content = List.map snd filtered in
555
      (* Elements are supposed to be a pair (tuple): variable, expression *)
556 5cf953ec tkahsai
      List.map (fun ee ->
557
	match ee.eexpr_quantifiers, ee.eexpr_qfexpr.expr_desc with
558 af5af1e8 ploc
	| [], Expr_tuple [v;e] -> (
559 5cf953ec tkahsai
	  match v.expr_desc with
560
	  | Expr_ident vid -> vid, e
561 af5af1e8 ploc
	  | _ -> assert false )
562
	| _ -> assert false)
563
	content
564
    in
565 5cf953ec tkahsai
566 af5af1e8 ploc
    m, traces
567
568
  ) machines
569
  in
570
571
  (* Compute memories associated to each machine *)
572
  let compute_mems m =
573
    let rec aux fst prefix m =
574
      (List.map (fun mem -> (prefix, mem)) m.mmemory) @
575 5cf953ec tkahsai
	List.fold_left (fun accu (id, (n, _)) ->
576
	  let name = node_name n in
577 af5af1e8 ploc
	  if name = "_arrow" then accu else
578
	    let machine_n = get_machine machines name in
579 5cf953ec tkahsai
	    ( aux false ((id,machine_n)::prefix) machine_n )
580 af5af1e8 ploc
	    @ accu
581 5cf953ec tkahsai
	) [] m.minstances
582 af5af1e8 ploc
    in
583
    aux true [] m
584
  in
585
586
  List.iter (fun m ->
587
    Format.fprintf fmt "; Node %s@." m.mname.node_id;
588 5cf953ec tkahsai
589
    let memories_old =
590
      List.map (fun (p, v) ->
591 af5af1e8 ploc
	let machine = match p with | [] -> m | (_,m')::_ -> m' in
592
	let traces = List.assoc machine machines_traces in
593 3ca6d126 ploc
	if List.mem_assoc v.var_id traces then (
594 af5af1e8 ploc
	  (* We take the expression associated to variable v in the trace info *)
595 3ca6d126 ploc
	  (* Format.eprintf "Found variable %a in traces: %a@."  pp_var v Printers.pp_expr (List.assoc v.var_id traces); *)
596 af5af1e8 ploc
	  p, List.assoc v.var_id traces
597 3ca6d126 ploc
      )
598
	else (
599 af5af1e8 ploc
	  (* We keep the variable as is: we create an expression v *)
600 3ca6d126 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); *)
601 af5af1e8 ploc
	  p, mkexpr Location.dummy_loc (Expr_ident v.var_id)
602 3ca6d126 ploc
	)
603 5cf953ec tkahsai
604
      ) (compute_mems m)
605 af5af1e8 ploc
    in
606
    let memories_next = (* We remove the topest pre in each expression *)
607 5cf953ec tkahsai
      List.map
608 3ca6d126 ploc
      	(fun (prefix, ee) ->
609
      	  match ee.expr_desc with
610
      	  | Expr_pre e -> prefix, e
611
      	  | _ -> Format.eprintf
612
      	    "Mem Failure: (prefix: %a, eexpr: %a)@.@?"
613
      	    (Utils.fprintf_list ~sep:","
614
      	       (fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id ))
615
      	    (List.rev prefix)
616
      	    Printers.pp_expr ee;
617
      	    assert false)
618 af5af1e8 ploc
	memories_old
619
    in
620
621
    let pp_prefix_rev fmt prefix =
622
      Utils.fprintf_list ~sep:"." (fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id) fmt (List.rev prefix)
623
    in
624
625
    Format.fprintf fmt "; Init predicate@.";
626
627
    Format.fprintf fmt "; horn encoding@.";
628
    Format.fprintf fmt "(%a %a)@."
629
      pp_machine_init_name m.mname.node_id
630
      (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m);
631
632
    Format.fprintf fmt "; original expressions@.";
633
    Format.fprintf fmt "(%a %a%t%a)@."
634
      pp_machine_init_name m.mname.node_id
635
      (Utils.fprintf_list ~sep:" " pp_var) (m.mstep.step_inputs@m.mstep.step_outputs)
636
      (fun fmt -> match memories_next with [] -> () | _ -> fprintf fmt " ")
637
      (Utils.fprintf_list ~sep:" " (fun fmt (prefix, ee) -> fprintf fmt "%a(%a)" pp_prefix_rev prefix Printers.pp_expr ee)) memories_next;
638
639
    Format.pp_print_newline fmt ();
640
    Format.fprintf fmt "; Step predicate@.";
641
642
    Format.fprintf fmt "; horn encoding@.";
643
    Format.fprintf fmt "(%a %a)@."
644
      pp_machine_step_name m.mname.node_id
645
      (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m);
646
    Format.fprintf fmt "; original expressions@.";
647
    Format.fprintf fmt "(%a %a%t%a)@."
648
      pp_machine_step_name m.mname.node_id
649
      (Utils.fprintf_list ~sep:" " pp_var) (m.mstep.step_inputs@m.mstep.step_outputs)
650
      (fun fmt -> match memories_old with [] -> () | _ -> fprintf fmt " ")
651
      (Utils.fprintf_list ~sep:" " (fun fmt (prefix,ee) -> fprintf fmt "%a(%a)" pp_prefix_rev prefix Printers.pp_expr ee)) (memories_old@memories_next);
652 5cf953ec tkahsai
    Format.pp_print_newline fmt ();
653 af5af1e8 ploc
  ) (List.rev machines);
654 5cf953ec tkahsai
655 af5af1e8 ploc
656 dcbf9d3a ploc
(* Local Variables: *)
657 3ca6d126 ploc
(* compile-command:"make -C ../.." *)
658 dcbf9d3a ploc
(* End: *)