lustrec / src / backends / Horn / horn_backend.ml @ a1daa793
History | View | Annotate | Download (24.8 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 |
|
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 |
(* 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 |
match instr with |
245 |
| MReset i -> |
246 |
pp_machine_init m self fmt i |
247 |
| 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 |
| MStep ([i0], i, vl) when Basic_library.is_internal_fun i -> |
256 |
assert false (* This should not happen anymore *) |
257 |
| 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 |
(* may disappear if we optimize code by replacing last branch test with default *) |
263 |
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 |
|
271 |
let is_stateless m = m.minstances = [] && m.mmemory = [] |
272 |
|
273 |
(* Print the machine m: |
274 |
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 |
let print_machine machines fmt m = |
280 |
let pp_instr init = pp_machine_instr machines ~init:init m in |
281 |
if m.mname.node_id = arrow_id then |
282 |
(* We don't print arrow function *) |
283 |
() |
284 |
else |
285 |
begin |
286 |
Format.fprintf fmt "; %s@." m.mname.node_id; |
287 |
|
288 |
(* Printing variables *) |
289 |
Utils.fprintf_list ~sep:"@." pp_decl_var fmt |
290 |
((step_vars machines m)@ |
291 |
(rename_machine_list m.mname.node_id m.mstep.step_locals)); |
292 |
Format.pp_print_newline fmt (); |
293 |
|
294 |
|
295 |
|
296 |
if is_stateless m then |
297 |
begin |
298 |
(* Declaring single predicate *) |
299 |
Format.fprintf fmt "(declare-rel %a (%a))@." |
300 |
pp_machine_stateless_name m.mname.node_id |
301 |
(Utils.fprintf_list ~sep:" " pp_type) |
302 |
(List.map (fun v -> v.var_type) (stateless_vars machines m)); |
303 |
|
304 |
(* Rule for single predicate *) |
305 |
Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@." |
306 |
(pp_conj (pp_instr |
307 |
true (* In this case, the boolean init can be set to true or false. |
308 |
The node is stateless. *) |
309 |
m.mname.node_id) |
310 |
) |
311 |
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 |
else |
316 |
begin |
317 |
(* Declaring predicate *) |
318 |
Format.fprintf fmt "(declare-rel %a (%a))@." |
319 |
pp_machine_init_name m.mname.node_id |
320 |
(Utils.fprintf_list ~sep:" " pp_type) |
321 |
(List.map (fun v -> v.var_type) (init_vars machines m)); |
322 |
|
323 |
Format.fprintf fmt "(declare-rel %a (%a))@." |
324 |
pp_machine_step_name m.mname.node_id |
325 |
(Utils.fprintf_list ~sep:" " pp_type) |
326 |
(List.map (fun v -> v.var_type) (step_vars machines m)); |
327 |
|
328 |
Format.pp_print_newline fmt (); |
329 |
|
330 |
(* Adding assertions *) |
331 |
(match m.mstep.step_asserts with |
332 |
| [] -> |
333 |
begin |
334 |
(* Rule for init *) |
335 |
Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@." |
336 |
(pp_conj (pp_instr true m.mname.node_id)) m.mstep.step_instrs |
337 |
pp_machine_init_name m.mname.node_id |
338 |
(Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m); |
339 |
(* Rule for step*) |
340 |
Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@." |
341 |
(pp_conj (pp_instr false m.mname.node_id)) m.mstep.step_instrs |
342 |
pp_machine_step_name m.mname.node_id |
343 |
(Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m); |
344 |
end |
345 |
| assertsl -> |
346 |
begin |
347 |
let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id pp_var in |
348 |
(* print_string pp_val; *) |
349 |
let instrs_concat = m.mstep.step_instrs in |
350 |
Format.fprintf fmt "; with Assertions @."; |
351 |
(*Rule for init*) |
352 |
Format.fprintf fmt "@[<v 2>(rule (=> @ (and @ %a@. %a)(%a %a)@]@.))@.@." |
353 |
(pp_conj (pp_instr true m.mname.node_id)) instrs_concat |
354 |
(pp_conj pp_val) assertsl |
355 |
pp_machine_init_name m.mname.node_id |
356 |
(Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m); |
357 |
(*Rule for step*) |
358 |
Format.fprintf fmt "@[<v 2>(rule (=> @ (and @ %a@. %a)(%a %a)@]@.))@.@." |
359 |
(pp_conj (pp_instr false m.mname.node_id)) instrs_concat |
360 |
(pp_conj pp_val) assertsl |
361 |
pp_machine_step_name m.mname.node_id |
362 |
(Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m); |
363 |
end |
364 |
); |
365 |
end |
366 |
end |
367 |
|
368 |
|
369 |
|
370 |
let collecting_semantics machines fmt node machine = |
371 |
Format.fprintf fmt "; Collecting semantics for node %s@.@." node; |
372 |
(* We print the types of the main node "memory tree" TODO: add the output *) |
373 |
let main_output = |
374 |
rename_machine_list machine.mname.node_id machine.mstep.step_outputs |
375 |
in |
376 |
let main_output_dummy = |
377 |
rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_outputs |
378 |
in |
379 |
let main_memory_next = |
380 |
(rename_next_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @ |
381 |
main_output |
382 |
in |
383 |
let main_memory_current = |
384 |
(rename_current_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @ |
385 |
main_output_dummy |
386 |
in |
387 |
|
388 |
(* Special case when the main node is stateless *) |
389 |
let init_name, step_name = |
390 |
if is_stateless machine then |
391 |
pp_machine_stateless_name, pp_machine_stateless_name |
392 |
else |
393 |
pp_machine_init_name, pp_machine_step_name |
394 |
in |
395 |
|
396 |
Format.fprintf fmt "(declare-rel MAIN (%a))@." |
397 |
(Utils.fprintf_list ~sep:" " pp_type) |
398 |
(List.map (fun v -> v.var_type) main_memory_next); |
399 |
|
400 |
Format.fprintf fmt "; Initial set@."; |
401 |
Format.fprintf fmt "(declare-rel INIT_STATE ())@."; |
402 |
Format.fprintf fmt "(rule INIT_STATE)@."; |
403 |
Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>INIT_STATE@ (@[<v 0>%a %a@])@]@ )@ (MAIN %a)@]@.))@.@." |
404 |
init_name node |
405 |
(Utils.fprintf_list ~sep:" " pp_var) (init_vars machines machine) |
406 |
(Utils.fprintf_list ~sep:" " pp_var) main_memory_next ; |
407 |
|
408 |
Format.fprintf fmt "; Inductive def@."; |
409 |
(Utils.fprintf_list ~sep:" " (fun fmt v -> Format.fprintf fmt "%a@." pp_decl_var v)) fmt main_output_dummy; |
410 |
Format.fprintf fmt |
411 |
"@[<v 2>(rule (=> @ (and @[<v 0>(MAIN %a)@ (@[<v 0>%a %a@])@]@ )@ (MAIN %a)@]@.))@.@." |
412 |
(Utils.fprintf_list ~sep:" " pp_var) main_memory_current |
413 |
step_name node |
414 |
(Utils.fprintf_list ~sep:" " pp_var) (step_vars machines machine) |
415 |
(Utils.fprintf_list ~sep:" " pp_var) main_memory_next |
416 |
|
417 |
let check_prop machines fmt node machine = |
418 |
let main_output = |
419 |
rename_machine_list machine.mname.node_id machine.mstep.step_outputs |
420 |
in |
421 |
let main_memory_next = |
422 |
(rename_next_list (full_memory_vars machines machine)) @ main_output |
423 |
in |
424 |
Format.fprintf fmt "; Property def@."; |
425 |
Format.fprintf fmt "(declare-rel ERR ())@."; |
426 |
Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (MAIN %a)@])@ ERR))@." |
427 |
(pp_conj pp_var) main_output |
428 |
(Utils.fprintf_list ~sep:" " pp_var) main_memory_next |
429 |
; |
430 |
if !Options.horn_query then Format.fprintf fmt "(query ERR)@." |
431 |
|
432 |
|
433 |
let cex_computation machines fmt node machine = |
434 |
Format.fprintf fmt "; CounterExample computation for node %s@.@." node; |
435 |
(* We print the types of the cex node "memory tree" TODO: add the output *) |
436 |
let cex_input = |
437 |
rename_machine_list machine.mname.node_id machine.mstep.step_inputs |
438 |
in |
439 |
let cex_input_dummy = |
440 |
rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_inputs |
441 |
in |
442 |
let cex_output = |
443 |
rename_machine_list machine.mname.node_id machine.mstep.step_outputs |
444 |
in |
445 |
let cex_output_dummy = |
446 |
rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_outputs |
447 |
in |
448 |
let cex_memory_next = |
449 |
cex_input @ (rename_next_list (full_memory_vars machines machine)) @ cex_output |
450 |
in |
451 |
let cex_memory_current = |
452 |
cex_input_dummy @ (rename_current_list (full_memory_vars machines machine)) @ cex_output_dummy |
453 |
in |
454 |
|
455 |
(* Special case when the cex node is stateless *) |
456 |
let init_name, step_name = |
457 |
if is_stateless machine then |
458 |
pp_machine_stateless_name, pp_machine_stateless_name |
459 |
else |
460 |
pp_machine_init_name, pp_machine_step_name |
461 |
in |
462 |
|
463 |
Format.fprintf fmt "(declare-rel CEX (Int %a))@.@." |
464 |
(Utils.fprintf_list ~sep:" " pp_type) |
465 |
(List.map (fun v -> v.var_type) cex_memory_next); |
466 |
|
467 |
Format.fprintf fmt "; Initial set@."; |
468 |
Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>INIT_STATE@ (@[<v 0>%a %a@])@]@ )@ (CEX 0 %a)@]@.))@.@." |
469 |
init_name node |
470 |
(Utils.fprintf_list ~sep:" " pp_var) (init_vars machines machine) |
471 |
(Utils.fprintf_list ~sep:" " pp_var) cex_memory_next ; |
472 |
|
473 |
Format.fprintf fmt "; Inductive def@."; |
474 |
(* Declare dummy inputs. Outputs should have been declared previously with collecting sem *) |
475 |
(Utils.fprintf_list ~sep:" " (fun fmt v -> Format.fprintf fmt "%a@." pp_decl_var v)) fmt cex_input_dummy; |
476 |
Format.fprintf fmt "(declare-var cexcpt Int)@."; |
477 |
Format.fprintf fmt |
478 |
"@[<v 2>(rule (=> @ (and @[<v 0>(CEX cexcpt %a)@ (@[<v 0>%a %a@])@]@ )@ (CEX (+ 1 cexcpt) %a)@]@.))@.@." |
479 |
(Utils.fprintf_list ~sep:" " pp_var) cex_memory_current |
480 |
step_name node |
481 |
(Utils.fprintf_list ~sep:" " pp_var) (step_vars machines machine) |
482 |
(Utils.fprintf_list ~sep:" " pp_var) cex_memory_next |
483 |
|
484 |
let get_cex machines fmt node machine = |
485 |
let cex_input = |
486 |
rename_machine_list 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_memory_next = |
492 |
cex_input @ (rename_next_list (full_memory_vars machines machine)) @ cex_output |
493 |
in |
494 |
Format.fprintf fmt "; Property def@."; |
495 |
Format.fprintf fmt "(declare-rel CEXTRACE ())@."; |
496 |
Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (CEX cexcpt %a)@])@ CEXTRACE))@." |
497 |
(pp_conj pp_var) cex_output |
498 |
(Utils.fprintf_list ~sep:" " pp_var) cex_memory_next |
499 |
; |
500 |
Format.fprintf fmt "(query CEXTRACE)@." |
501 |
|
502 |
|
503 |
let main_print machines fmt = |
504 |
if !Options.main_node <> "" then |
505 |
begin |
506 |
let node = !Options.main_node in |
507 |
let machine = get_machine machines node in |
508 |
|
509 |
|
510 |
collecting_semantics machines fmt node machine; |
511 |
check_prop machines fmt node machine; |
512 |
if !Options.horn_cex then( |
513 |
cex_computation machines fmt node machine; |
514 |
get_cex machines fmt node machine) |
515 |
end |
516 |
|
517 |
|
518 |
let translate fmt basename prog machines = |
519 |
List.iter (print_machine machines fmt) (List.rev machines); |
520 |
main_print machines fmt |
521 |
|
522 |
|
523 |
let traces_file fmt basename prog machines = |
524 |
|
525 |
Format.fprintf fmt |
526 |
"<?xml version=\"1.0\"?>\n<Traces xmlns:xsi=\"http://www.w3.org/2001/XMLSchema-instance\">\n"; |
527 |
|
528 |
(* We extract the annotation dealing with traceability *) |
529 |
let machines_traces = List.map (fun m -> |
530 |
let traces : (ident * expr) list= |
531 |
let all_annots = List.flatten (List.map (fun ann -> ann.annots) m.mannot) in |
532 |
let filtered = |
533 |
List.filter (fun (kwds, _) -> kwds = ["traceability"]) all_annots |
534 |
in |
535 |
let content = List.map snd filtered in |
536 |
(* Elements are supposed to be a pair (tuple): variable, expression *) |
537 |
List.map (fun ee -> |
538 |
match ee.eexpr_quantifiers, ee.eexpr_qfexpr.expr_desc with |
539 |
| [], Expr_tuple [v;e] -> ( |
540 |
match v.expr_desc with |
541 |
| Expr_ident vid -> vid, e |
542 |
| _ -> assert false ) |
543 |
| _ -> assert false) |
544 |
content |
545 |
in |
546 |
|
547 |
m, traces |
548 |
|
549 |
) machines |
550 |
in |
551 |
|
552 |
(* Compute memories associated to each machine *) |
553 |
let compute_mems m = |
554 |
let rec aux fst prefix m = |
555 |
(List.map (fun mem -> (prefix, mem)) m.mmemory) @ |
556 |
List.fold_left (fun accu (id, (n, _)) -> |
557 |
let name = node_name n in |
558 |
if name = "_arrow" then accu else |
559 |
let machine_n = get_machine machines name in |
560 |
( aux false ((id,machine_n)::prefix) machine_n ) |
561 |
@ accu |
562 |
) [] m.minstances |
563 |
in |
564 |
aux true [] m |
565 |
in |
566 |
|
567 |
List.iter (fun m -> |
568 |
(* Format.fprintf fmt "; Node %s@." m.mname.node_id; *) |
569 |
Format.fprintf fmt " <Node name=\"%s\">@." m.mname.node_id; |
570 |
|
571 |
let memories_old = |
572 |
List.map (fun (p, v) -> |
573 |
let machine = match p with | [] -> m | (_,m')::_ -> m' in |
574 |
let traces = List.assoc machine machines_traces in |
575 |
if List.mem_assoc v.var_id traces then ( |
576 |
(* We take the expression associated to variable v in the trace info *) |
577 |
(* Format.eprintf "Found variable %a in traces: %a@." pp_var v Printers.pp_expr (List.assoc v.var_id traces); *) |
578 |
p, List.assoc v.var_id traces |
579 |
) |
580 |
else ( |
581 |
(* We keep the variable as is: we create an expression v *) |
582 |
(* 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); *) |
583 |
p, mkexpr Location.dummy_loc (Expr_ident v.var_id) |
584 |
) |
585 |
|
586 |
) (compute_mems m) |
587 |
in |
588 |
let memories_next = (* We remove the topest pre in each expression *) |
589 |
List.map |
590 |
(fun (prefix, ee) -> |
591 |
match ee.expr_desc with |
592 |
| Expr_pre e -> prefix, e |
593 |
| _ -> Format.eprintf |
594 |
"Mem Failure: (prefix: %a, eexpr: %a)@.@?" |
595 |
(Utils.fprintf_list ~sep:"," |
596 |
(fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id )) |
597 |
(List.rev prefix) |
598 |
Printers.pp_expr ee; |
599 |
assert false) |
600 |
memories_old |
601 |
in |
602 |
|
603 |
(* let pp_prefix_rev fmt prefix = *) |
604 |
(* Utils.fprintf_list ~sep:"." (fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id) fmt (List.rev prefix) *) |
605 |
(* in *) |
606 |
|
607 |
let pp_prefix_rev fmt prefix = |
608 |
Utils.fprintf_list ~sep:"." (fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id) fmt (List.rev prefix) |
609 |
in |
610 |
|
611 |
let input_vars = (rename_machine_list m.mname.node_id m.mstep.step_inputs) in |
612 |
let output_vars = (rename_machine_list m.mname.node_id m.mstep.step_outputs) in |
613 |
Format.fprintf fmt " <input name=\"%a\" type=\"%a\">%a</input> @." |
614 |
(Utils.fprintf_list ~sep:" | " pp_var) input_vars |
615 |
(Utils.fprintf_list ~sep:" | " (fun fmt id -> pp_type fmt id.var_type)) input_vars |
616 |
(Utils.fprintf_list ~sep:" | " pp_var) (m.mstep.step_inputs); |
617 |
|
618 |
Format.fprintf fmt " <output name=\"%a\" type=\"%a\">%a</output> @." |
619 |
(Utils.fprintf_list ~sep:" | " pp_var) output_vars |
620 |
(Utils.fprintf_list ~sep:" | " (fun fmt id -> pp_type fmt id.var_type)) output_vars |
621 |
(Utils.fprintf_list ~sep:" | " pp_var) (m.mstep.step_outputs); |
622 |
|
623 |
let init_local_vars = (rename_next_list (full_memory_vars machines m)) in |
624 |
let step_local_vars = (rename_current_list (full_memory_vars machines m)) in |
625 |
|
626 |
Format.fprintf fmt " <localInit name=\"%a\" type=\"%a\">%t%a</localInit> @." |
627 |
(Utils.fprintf_list ~sep:" | " pp_var) init_local_vars |
628 |
(Utils.fprintf_list ~sep:" | " (fun fmt id -> pp_type fmt id.var_type)) init_local_vars |
629 |
(fun fmt -> match memories_next with [] -> () | _ -> fprintf fmt "") |
630 |
(Utils.fprintf_list ~sep:" | " (fun fmt (prefix, ee) -> fprintf fmt "%a" Printers.pp_expr ee)) memories_next; |
631 |
|
632 |
Format.fprintf fmt " <localStep name=\"%a\" type=\"%a\">%t%a</localStep> @." |
633 |
(Utils.fprintf_list ~sep:" | " pp_var) step_local_vars |
634 |
(Utils.fprintf_list ~sep:" | " (fun fmt id -> pp_type fmt id.var_type)) step_local_vars |
635 |
(fun fmt -> match memories_old with [] -> () | _ -> fprintf fmt "") |
636 |
(Utils.fprintf_list ~sep:" | " (fun fmt (prefix,ee) -> fprintf fmt "(%a)" |
637 |
Printers.pp_expr ee)) (memories_old); |
638 |
|
639 |
Format.fprintf fmt " </Node>@."; |
640 |
|
641 |
) (List.rev machines); |
642 |
Format.fprintf fmt "</Traces>@."; |
643 |
|
644 |
(* (Utils.fprintf_list ~sep:" | " (fun fmt (prefix, ee) -> fprintf fmt "%a%a" pp_prefix_rev prefix Printers.pp_expr ee)) memories_next; *) |
645 |
(* (Utils.fprintf_list ~sep:" | " (fun fmt (prefix,ee) -> fprintf fmt "%a(%a)" *) |
646 |
(* pp_prefix_rev prefix Printers.pp_expr ee)) (memories_old); *) |
647 |
|
648 |
(* Local Variables: *) |
649 |
(* compile-command:"make -C ../.." *) |
650 |
(* End: *) |