Revision 3c862628
Added by Teme Kahsai almost 10 years ago
src/backends/Horn/horn_backend.ml | ||
---|---|---|
32 | 32 |
| Types.Tstatic _ |
33 | 33 |
| Types.Tconst _ |
34 | 34 |
| Types.Tarrow _ |
35 |
| _ -> Format.eprintf "internal error: pp_type %a@."
|
|
35 |
| _ -> Format.eprintf "internal error: pp_type %a@." |
|
36 | 36 |
Types.print_ty t; assert false |
37 | 37 |
|
38 |
let pp_decl_var fmt id =
|
|
38 |
let pp_decl_var fmt id = |
|
39 | 39 |
Format.fprintf fmt "(declare-var %s %a)" |
40 | 40 |
id.var_id |
41 | 41 |
pp_type id.var_type |
... | ... | |
43 | 43 |
let pp_var fmt id = Format.pp_print_string fmt id.var_id |
44 | 44 |
|
45 | 45 |
|
46 |
let pp_conj pp fmt l =
|
|
47 |
match l with
|
|
46 |
let pp_conj pp fmt l = |
|
47 |
match l with |
|
48 | 48 |
[] -> assert false |
49 | 49 |
| [x] -> pp fmt x |
50 | 50 |
| _ -> fprintf fmt "(and @[<v 0>%a@]@ )" (Utils.fprintf_list ~sep:" " pp) l |
51 |
|
|
52 | 51 |
|
53 | 52 |
|
54 |
let concat prefix x = if prefix = "" then x else prefix ^ "." ^ x |
|
53 |
|
|
54 |
let concat prefix x = if prefix = "" then x else prefix ^ "." ^ x |
|
55 | 55 |
let rename f = (fun v -> {v with var_id = f v.var_id } ) |
56 | 56 |
let rename_machine p = rename (fun n -> concat p n) |
57 | 57 |
let rename_machine_list p = List.map (rename_machine p) |
58 |
|
|
58 |
|
|
59 | 59 |
let rename_current = rename (fun n -> n ^ "_c") |
60 | 60 |
let rename_current_list = List.map rename_current |
61 | 61 |
let rename_next = rename (fun n -> n ^ "_x") |
62 | 62 |
let rename_next_list = List.map rename_next |
63 | 63 |
|
64 | 64 |
|
65 |
let get_machine machines node_name =
|
|
66 |
List.find (fun m -> m.mname.node_id = node_name) machines
|
|
65 |
let get_machine machines node_name = |
|
66 |
List.find (fun m -> m.mname.node_id = node_name) machines |
|
67 | 67 |
|
68 | 68 |
let full_memory_vars machines machine = |
69 | 69 |
let rec aux fst prefix m = |
70 | 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
|
|
71 |
List.fold_left (fun accu (id, (n, _)) -> |
|
72 |
let name = node_name n in |
|
73 | 73 |
if name = "_arrow" then accu else |
74 | 74 |
let machine_n = get_machine machines name in |
75 | 75 |
( aux false (concat prefix (if fst then id else concat m.mname.node_id id)) machine_n ) @ accu |
76 |
) [] (m.minstances)
|
|
76 |
) [] (m.minstances) |
|
77 | 77 |
in |
78 | 78 |
aux true machine.mname.node_id machine |
79 | 79 |
|
80 |
let stateless_vars machines m =
|
|
80 |
let stateless_vars machines m = |
|
81 | 81 |
(rename_machine_list m.mname.node_id m.mstep.step_inputs)@ |
82 | 82 |
(rename_machine_list m.mname.node_id m.mstep.step_outputs) |
83 |
|
|
84 |
let step_vars machines m =
|
|
83 |
|
|
84 |
let step_vars machines m = |
|
85 | 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 |
|
|
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 | 92 |
(********************************************************************************************) |
93 | 93 |
(* Instruction Printing functions *) |
94 | 94 |
(********************************************************************************************) |
... | ... | |
121 | 121 |
let rec pp_horn_val ?(is_lhs=false) self pp_var fmt v = |
122 | 122 |
match v with |
123 | 123 |
| Cst c -> pp_horn_const fmt c |
124 |
| Array _
|
|
124 |
| Array _ |
|
125 | 125 |
| Access _ -> assert false (* no arrays *) |
126 | 126 |
| Power (v, n) -> assert false |
127 | 127 |
| LocalVar v -> pp_var fmt (rename_machine self v) |
128 | 128 |
| StateVar v -> |
129 | 129 |
if Types.is_array_type v.var_type |
130 |
then assert false
|
|
130 |
then assert false |
|
131 | 131 |
else pp_var fmt (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v)) |
132 | 132 |
| Fun (n, vl) -> Format.fprintf fmt "%a" (Basic_library.pp_horn n (pp_horn_val self pp_var)) vl |
133 | 133 |
|
... | ... | |
147 | 147 |
*) |
148 | 148 |
let pp_assign m self pp_var fmt var_type var_name value = |
149 | 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
|
|
150 |
|
|
151 |
let pp_instance_call |
|
152 | 152 |
machines ?(init=false) m self fmt i (inputs: value_t list) (outputs: var_decl list) = |
153 |
try (* stateful node instance *)
|
|
153 |
try (* stateful node instance *) |
|
154 | 154 |
begin |
155 | 155 |
let (n,_) = List.assoc i m.minstances in |
156 | 156 |
match node_name n, inputs, outputs with |
... | ... | |
159 | 159 |
pp_assign |
160 | 160 |
m |
161 | 161 |
self |
162 |
(pp_horn_var m)
|
|
162 |
(pp_horn_var m) |
|
163 | 163 |
fmt |
164 | 164 |
o.var_type (LocalVar o) i1 |
165 | 165 |
else |
166 | 166 |
pp_assign |
167 | 167 |
m self (pp_horn_var m) fmt |
168 | 168 |
o.var_type (LocalVar o) i2 |
169 |
|
|
169 |
|
|
170 | 170 |
end |
171 |
| name, _, _ ->
|
|
171 |
| name, _, _ -> |
|
172 | 172 |
begin |
173 | 173 |
let target_machine = List.find (fun m -> m.mname.node_id = name) machines in |
174 | 174 |
if init then |
175 | 175 |
Format.fprintf fmt "(%a %a%t%a%t%a)" |
176 |
pp_machine_init_name (node_name n)
|
|
176 |
pp_machine_init_name (node_name n) |
|
177 | 177 |
(* inputs *) |
178 |
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m)))
|
|
178 |
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) |
|
179 | 179 |
inputs |
180 |
(Utils.pp_final_char_if_non_empty " " inputs)
|
|
180 |
(Utils.pp_final_char_if_non_empty " " inputs) |
|
181 | 181 |
(* outputs *) |
182 |
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m)))
|
|
182 |
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) |
|
183 | 183 |
(List.map (fun v -> LocalVar v) outputs) |
184 | 184 |
(Utils.pp_final_char_if_non_empty " " outputs) |
185 | 185 |
(* memories (next) *) |
186 | 186 |
(Utils.fprintf_list ~sep:" " pp_var) ( |
187 |
rename_machine_list
|
|
188 |
(concat m.mname.node_id i)
|
|
187 |
rename_machine_list |
|
188 |
(concat m.mname.node_id i) |
|
189 | 189 |
(rename_next_list (full_memory_vars machines target_machine) |
190 |
)
|
|
190 |
) |
|
191 | 191 |
) |
192 | 192 |
else |
193 | 193 |
Format.fprintf fmt "(%a %a%t%a%t%a)" |
194 |
pp_machine_step_name (node_name n)
|
|
194 |
pp_machine_step_name (node_name n) |
|
195 | 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)))
|
|
196 |
(Utils.pp_final_char_if_non_empty " " inputs) |
|
197 |
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) |
|
198 | 198 |
(List.map (fun v -> LocalVar v) outputs) |
199 | 199 |
(Utils.pp_final_char_if_non_empty " " outputs) |
200 | 200 |
(Utils.fprintf_list ~sep:" " pp_var) ( |
201 |
(rename_machine_list
|
|
202 |
(concat m.mname.node_id i)
|
|
201 |
(rename_machine_list |
|
202 |
(concat m.mname.node_id i) |
|
203 | 203 |
(rename_current_list (full_memory_vars machines target_machine)) |
204 |
) @
|
|
205 |
(rename_machine_list
|
|
206 |
(concat m.mname.node_id i)
|
|
204 |
) @ |
|
205 |
(rename_machine_list |
|
206 |
(concat m.mname.node_id i) |
|
207 | 207 |
(rename_next_list (full_memory_vars machines target_machine)) |
208 |
)
|
|
208 |
) |
|
209 | 209 |
) |
210 |
|
|
210 |
|
|
211 | 211 |
end |
212 | 212 |
end |
213 | 213 |
with Not_found -> ( (* stateless node instance *) |
214 | 214 |
let (n,_) = List.assoc i m.mcalls in |
215 | 215 |
Format.fprintf fmt "(%s %a%t%a)" |
216 | 216 |
(node_name n) |
217 |
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m)))
|
|
217 |
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) |
|
218 | 218 |
inputs |
219 |
(Utils.pp_final_char_if_non_empty " " inputs)
|
|
220 |
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m)))
|
|
219 |
(Utils.pp_final_char_if_non_empty " " inputs) |
|
220 |
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) |
|
221 | 221 |
(List.map (fun v -> LocalVar v) outputs) |
222 | 222 |
) |
223 | 223 |
|
... | ... | |
239 | 239 |
(Utils.fprintf_list ~sep:"@," (pp_machine_instr machines ~init:init m self)) el |
240 | 240 |
|
241 | 241 |
and pp_machine_instr machines ?(init=false) (m: machine_t) self fmt instr = |
242 |
match instr with
|
|
242 |
match instr with |
|
243 | 243 |
| MReset i -> |
244 | 244 |
pp_machine_init m self fmt i |
245 | 245 |
| MLocalAssign (i,v) -> |
... | ... | |
250 | 250 |
pp_assign |
251 | 251 |
m self (pp_horn_var m) fmt |
252 | 252 |
i.var_type (StateVar i) v |
253 |
| MStep ([i0], i, vl) when Basic_library.is_internal_fun i ->
|
|
253 |
| MStep ([i0], i, vl) when Basic_library.is_internal_fun i -> |
|
254 | 254 |
assert false (* This should not happen anymore *) |
255 | 255 |
| MStep (il, i, vl) -> |
256 | 256 |
pp_instance_call machines ~init:init m self fmt i vl il |
... | ... | |
265 | 265 |
|
266 | 266 |
|
267 | 267 |
(**************************************************************) |
268 |
|
|
269 |
let is_stateless m = m.minstances = [] && m.mmemory = [] |
|
270 | 268 |
|
271 |
(* Print the machine m: |
|
269 |
let is_stateless m = m.minstances = [] && m.mmemory = [] |
|
270 |
|
|
271 |
(* Print the machine m: |
|
272 | 272 |
two functions: m_init and m_step |
273 | 273 |
- m_init is a predicate over m memories |
274 | 274 |
- m_step is a predicate over old_memories, inputs, new_memories, outputs |
275 | 275 |
We first declare all variables then the two /rules/. |
276 | 276 |
*) |
277 |
let print_machine machines fmt m =
|
|
277 |
let print_machine machines fmt m = |
|
278 | 278 |
let pp_instr init = pp_machine_instr machines ~init:init m in |
279 |
if m.mname.node_id = arrow_id then
|
|
279 |
if m.mname.node_id = arrow_id then |
|
280 | 280 |
(* We don't print arrow function *) |
281 | 281 |
() |
282 |
else
|
|
283 |
begin
|
|
282 |
else |
|
283 |
begin |
|
284 | 284 |
Format.fprintf fmt "; %s@." m.mname.node_id; |
285 | 285 |
|
286 | 286 |
(* Printing variables *) |
287 |
Utils.fprintf_list ~sep:"@." pp_decl_var fmt
|
|
287 |
Utils.fprintf_list ~sep:"@." pp_decl_var fmt |
|
288 | 288 |
((step_vars machines m)@ |
289 | 289 |
(rename_machine_list m.mname.node_id m.mstep.step_locals)); |
290 | 290 |
Format.pp_print_newline fmt (); |
291 | 291 |
|
292 |
|
|
293 |
|
|
292 |
|
|
293 |
|
|
294 | 294 |
if is_stateless m then |
295 | 295 |
begin |
296 | 296 |
(* Declaring single predicate *) |
297 | 297 |
Format.fprintf fmt "(declare-rel %a (%a))@." |
298 | 298 |
pp_machine_stateless_name m.mname.node_id |
299 |
(Utils.fprintf_list ~sep:" " pp_type)
|
|
299 |
(Utils.fprintf_list ~sep:" " pp_type) |
|
300 | 300 |
(List.map (fun v -> v.var_type) (stateless_vars machines m)); |
301 |
|
|
301 |
|
|
302 | 302 |
(* Rule for single predicate *) |
303 | 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.
|
|
304 |
(pp_conj (pp_instr |
|
305 |
true (* In this case, the boolean init can be set to true or false. |
|
306 | 306 |
The node is stateless. *) |
307 | 307 |
m.mname.node_id) |
308 | 308 |
) |
... | ... | |
310 | 310 |
pp_machine_stateless_name m.mname.node_id |
311 | 311 |
(Utils.fprintf_list ~sep:" " pp_var) (stateless_vars machines m); |
312 | 312 |
end |
313 |
else
|
|
313 |
else |
|
314 | 314 |
begin |
315 | 315 |
(* Declaring predicate *) |
316 | 316 |
Format.fprintf fmt "(declare-rel %a (%a))@." |
317 | 317 |
pp_machine_init_name m.mname.node_id |
318 |
(Utils.fprintf_list ~sep:" " pp_type)
|
|
318 |
(Utils.fprintf_list ~sep:" " pp_type) |
|
319 | 319 |
(List.map (fun v -> v.var_type) (init_vars machines m)); |
320 |
|
|
320 |
|
|
321 | 321 |
Format.fprintf fmt "(declare-rel %a (%a))@." |
322 | 322 |
pp_machine_step_name m.mname.node_id |
323 |
(Utils.fprintf_list ~sep:" " pp_type)
|
|
323 |
(Utils.fprintf_list ~sep:" " pp_type) |
|
324 | 324 |
(List.map (fun v -> v.var_type) (step_vars machines m)); |
325 |
|
|
325 |
|
|
326 | 326 |
Format.pp_print_newline fmt (); |
327 | 327 |
|
328 | 328 |
(* Rule for init *) |
... | ... | |
342 | 342 |
| [] -> () |
343 | 343 |
| assertsl -> begin |
344 | 344 |
let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id pp_var in |
345 |
|
|
345 |
|
|
346 | 346 |
Format.fprintf fmt "; Asserts@."; |
347 | 347 |
Format.fprintf fmt "(assert @[<v 2>%a@]@ )@.@.@." |
348 | 348 |
(pp_conj pp_val) assertsl; |
349 |
|
|
350 |
(** TEME: the following code is the one we described. But it generates a segfault in z3
|
|
349 |
|
|
350 |
(** TEME: the following code is the one we described. But it generates a segfault in z3 |
|
351 | 351 |
Format.fprintf fmt "; Asserts for init@."; |
352 | 352 |
Format.fprintf fmt "@[<v 2>(assert (=> @ (and @[<v 0>%a@]@ (%a %a))@ %a@]@.))@.@.@." |
353 | 353 |
(Utils.fprintf_list ~sep:"@ " (pp_instr true m.mname.node_id)) m.mstep.step_instrs |
354 | 354 |
pp_machine_init_name m.mname.node_id |
355 | 355 |
(Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m) |
356 |
(pp_conj pp_val) assertsl;
|
|
357 |
|
|
356 |
(pp_conj pp_val) assertsl; |
|
357 |
|
|
358 | 358 |
Format.fprintf fmt "; Asserts for step@."; |
359 | 359 |
Format.fprintf fmt "@[<v 2>(assert (=> @ (and @[<v 0>%a@]@ (%a %a))@ %a@]@.))@.@." |
360 | 360 |
(Utils.fprintf_list ~sep:"@ " (pp_instr false m.mname.node_id)) m.mstep.step_instrs |
... | ... | |
365 | 365 |
*) |
366 | 366 |
end |
367 | 367 |
); |
368 |
|
|
368 |
|
|
369 | 369 |
(* |
370 | 370 |
match m.mspec with |
371 | 371 |
None -> () (* No node spec; we do nothing *) |
372 |
| Some {requires = []; ensures = [EnsuresExpr e]; behaviors = []} ->
|
|
373 |
(
|
|
372 |
| Some {requires = []; ensures = [EnsuresExpr e]; behaviors = []} -> |
|
373 |
( |
|
374 | 374 |
(* For the moment, we only deal with simple case: single ensures, no other parameters *) |
375 | 375 |
() |
376 |
|
|
376 |
|
|
377 | 377 |
) |
378 | 378 |
| _ -> () (* Other cases give nothing *) |
379 |
*)
|
|
379 |
*) |
|
380 | 380 |
end |
381 | 381 |
end |
382 | 382 |
|
... | ... | |
388 | 388 |
let main_output = |
389 | 389 |
rename_machine_list machine.mname.node_id machine.mstep.step_outputs |
390 | 390 |
in |
391 |
let main_output_dummy =
|
|
391 |
let main_output_dummy = |
|
392 | 392 |
rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_outputs |
393 | 393 |
in |
394 |
let main_memory_next =
|
|
394 |
let main_memory_next = |
|
395 | 395 |
(rename_next_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @ |
396 | 396 |
main_output |
397 | 397 |
in |
398 |
let main_memory_current =
|
|
398 |
let main_memory_current = |
|
399 | 399 |
(rename_current_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @ |
400 | 400 |
main_output_dummy |
401 | 401 |
in |
402 | 402 |
|
403 | 403 |
(* Special case when the main node is stateless *) |
404 |
let init_name, step_name =
|
|
404 |
let init_name, step_name = |
|
405 | 405 |
if is_stateless machine then |
406 | 406 |
pp_machine_stateless_name, pp_machine_stateless_name |
407 | 407 |
else |
... | ... | |
409 | 409 |
in |
410 | 410 |
|
411 | 411 |
Format.fprintf fmt "(declare-rel MAIN (%a))@." |
412 |
(Utils.fprintf_list ~sep:" " pp_type)
|
|
412 |
(Utils.fprintf_list ~sep:" " pp_type) |
|
413 | 413 |
(List.map (fun v -> v.var_type) main_memory_next); |
414 |
|
|
414 |
|
|
415 | 415 |
Format.fprintf fmt "; Initial set@."; |
416 | 416 |
Format.fprintf fmt "(declare-rel INIT_STATE ())@."; |
417 | 417 |
Format.fprintf fmt "(rule INIT_STATE)@."; |
... | ... | |
422 | 422 |
|
423 | 423 |
Format.fprintf fmt "; Inductive def@."; |
424 | 424 |
(Utils.fprintf_list ~sep:" " (fun fmt v -> Format.fprintf fmt "%a@." pp_decl_var v)) fmt main_output_dummy; |
425 |
Format.fprintf fmt
|
|
425 |
Format.fprintf fmt |
|
426 | 426 |
"@[<v 2>(rule (=> @ (and @[<v 0>(MAIN %a)@ (@[<v 0>%a %a@])@]@ )@ (MAIN %a)@]@.))@.@." |
427 | 427 |
(Utils.fprintf_list ~sep:" " pp_var) main_memory_current |
428 | 428 |
step_name node |
429 | 429 |
(Utils.fprintf_list ~sep:" " pp_var) (step_vars machines machine) |
430 |
(Utils.fprintf_list ~sep:" " pp_var) main_memory_next
|
|
430 |
(Utils.fprintf_list ~sep:" " pp_var) main_memory_next |
|
431 | 431 |
|
432 | 432 |
let check_prop machines fmt node machine = |
433 | 433 |
let main_output = |
434 | 434 |
rename_machine_list machine.mname.node_id machine.mstep.step_outputs |
435 | 435 |
in |
436 |
let main_memory_next =
|
|
436 |
let main_memory_next = |
|
437 | 437 |
(rename_next_list (full_memory_vars machines machine)) @ main_output |
438 | 438 |
in |
439 | 439 |
Format.fprintf fmt "; Property def@."; |
... | ... | |
452 | 452 |
let cex_input = |
453 | 453 |
rename_machine_list machine.mname.node_id machine.mstep.step_inputs |
454 | 454 |
in |
455 |
let cex_input_dummy =
|
|
455 |
let cex_input_dummy = |
|
456 | 456 |
rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_inputs |
457 | 457 |
in |
458 | 458 |
let cex_output = |
459 | 459 |
rename_machine_list machine.mname.node_id machine.mstep.step_outputs |
460 | 460 |
in |
461 |
let cex_output_dummy =
|
|
461 |
let cex_output_dummy = |
|
462 | 462 |
rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_outputs |
463 | 463 |
in |
464 |
let cex_memory_next =
|
|
464 |
let cex_memory_next = |
|
465 | 465 |
cex_input @ (rename_next_list (full_memory_vars machines machine)) @ cex_output |
466 | 466 |
in |
467 |
let cex_memory_current =
|
|
467 |
let cex_memory_current = |
|
468 | 468 |
cex_input_dummy @ (rename_current_list (full_memory_vars machines machine)) @ cex_output_dummy |
469 | 469 |
in |
470 | 470 |
|
471 | 471 |
(* Special case when the cex node is stateless *) |
472 |
let init_name, step_name =
|
|
472 |
let init_name, step_name = |
|
473 | 473 |
if is_stateless machine then |
474 | 474 |
pp_machine_stateless_name, pp_machine_stateless_name |
475 | 475 |
else |
... | ... | |
477 | 477 |
in |
478 | 478 |
|
479 | 479 |
Format.fprintf fmt "(declare-rel CEX (Int %a))@.@." |
480 |
(Utils.fprintf_list ~sep:" " pp_type)
|
|
480 |
(Utils.fprintf_list ~sep:" " pp_type) |
|
481 | 481 |
(List.map (fun v -> v.var_type) cex_memory_next); |
482 |
|
|
482 |
|
|
483 | 483 |
Format.fprintf fmt "; Initial set@."; |
484 | 484 |
Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>INIT_STATE@ (@[<v 0>%a %a@])@]@ )@ (CEX 0 %a)@]@.))@.@." |
485 | 485 |
init_name node |
... | ... | |
490 | 490 |
(* Declare dummy inputs. Outputs should have been declared previously with collecting sem *) |
491 | 491 |
(Utils.fprintf_list ~sep:" " (fun fmt v -> Format.fprintf fmt "%a@." pp_decl_var v)) fmt cex_input_dummy; |
492 | 492 |
Format.fprintf fmt "(declare-var cexcpt Int)@."; |
493 |
Format.fprintf fmt
|
|
493 |
Format.fprintf fmt |
|
494 | 494 |
"@[<v 2>(rule (=> @ (and @[<v 0>(CEX cexcpt %a)@ (@[<v 0>%a %a@])@]@ )@ (CEX (+ 1 cexcpt) %a)@]@.))@.@." |
495 | 495 |
(Utils.fprintf_list ~sep:" " pp_var) cex_memory_current |
496 | 496 |
step_name node |
497 | 497 |
(Utils.fprintf_list ~sep:" " pp_var) (step_vars machines machine) |
498 |
(Utils.fprintf_list ~sep:" " pp_var) cex_memory_next
|
|
498 |
(Utils.fprintf_list ~sep:" " pp_var) cex_memory_next |
|
499 | 499 |
|
500 | 500 |
let get_cex machines fmt node machine = |
501 | 501 |
let cex_input = |
... | ... | |
504 | 504 |
let cex_output = |
505 | 505 |
rename_machine_list machine.mname.node_id machine.mstep.step_outputs |
506 | 506 |
in |
507 |
let cex_memory_next =
|
|
507 |
let cex_memory_next = |
|
508 | 508 |
cex_input @ (rename_next_list (full_memory_vars machines machine)) @ cex_output |
509 | 509 |
in |
510 | 510 |
Format.fprintf fmt "; Property def@."; |
... | ... | |
517 | 517 |
Format.fprintf fmt "(query CEXTRACE)@." |
518 | 518 |
|
519 | 519 |
|
520 |
let main_print machines fmt =
|
|
521 |
if !Options.main_node <> "" then
|
|
520 |
let main_print machines fmt = |
|
521 |
if !Options.main_node <> "" then |
|
522 | 522 |
begin |
523 | 523 |
let node = !Options.main_node in |
524 | 524 |
let machine = get_machine machines node in |
... | ... | |
534 | 534 |
|
535 | 535 |
let translate fmt basename prog machines = |
536 | 536 |
List.iter (print_machine machines fmt) (List.rev machines); |
537 |
|
|
538 |
main_print machines fmt
|
|
537 |
|
|
538 |
main_print machines fmt |
|
539 | 539 |
|
540 | 540 |
|
541 | 541 |
let traces_file fmt basename prog machines = |
542 |
Format.fprintf fmt
|
|
542 |
Format.fprintf fmt |
|
543 | 543 |
"; Horn code traceability generated by %s@.; SVN version number %s@.@." |
544 |
(Filename.basename Sys.executable_name)
|
|
544 |
(Filename.basename Sys.executable_name) |
|
545 | 545 |
Version.number; |
546 | 546 |
|
547 | 547 |
(* We extract the annotation dealing with traceability *) |
548 |
let machines_traces = List.map (fun m ->
|
|
549 |
let traces : (ident * expr) list=
|
|
548 |
let machines_traces = List.map (fun m -> |
|
549 |
let traces : (ident * expr) list= |
|
550 | 550 |
let all_annots = List.flatten (List.map (fun ann -> ann.annots) m.mannot) in |
551 |
let filtered =
|
|
552 |
List.filter (fun (kwds, _) -> kwds = ["horn_backend";"trace"]) all_annots
|
|
551 |
let filtered = |
|
552 |
List.filter (fun (kwds, _) -> kwds = ["horn_backend";"trace"]) all_annots |
|
553 | 553 |
in |
554 | 554 |
let content = List.map snd filtered in |
555 | 555 |
(* Elements are supposed to be a pair (tuple): variable, expression *) |
556 |
List.map (fun ee ->
|
|
557 |
match ee.eexpr_quantifiers, ee.eexpr_qfexpr.expr_desc with
|
|
556 |
List.map (fun ee -> |
|
557 |
match ee.eexpr_quantifiers, ee.eexpr_qfexpr.expr_desc with |
|
558 | 558 |
| [], Expr_tuple [v;e] -> ( |
559 |
match v.expr_desc with
|
|
560 |
| Expr_ident vid -> vid, e
|
|
559 |
match v.expr_desc with |
|
560 |
| Expr_ident vid -> vid, e |
|
561 | 561 |
| _ -> assert false ) |
562 | 562 |
| _ -> assert false) |
563 | 563 |
content |
564 | 564 |
in |
565 |
|
|
565 |
|
|
566 | 566 |
m, traces |
567 | 567 |
|
568 | 568 |
) machines |
... | ... | |
572 | 572 |
let compute_mems m = |
573 | 573 |
let rec aux fst prefix m = |
574 | 574 |
(List.map (fun mem -> (prefix, mem)) m.mmemory) @ |
575 |
List.fold_left (fun accu (id, (n, _)) ->
|
|
576 |
let name = node_name n in
|
|
575 |
List.fold_left (fun accu (id, (n, _)) -> |
|
576 |
let name = node_name n in |
|
577 | 577 |
if name = "_arrow" then accu else |
578 | 578 |
let machine_n = get_machine machines name in |
579 |
( aux false ((id,machine_n)::prefix) machine_n )
|
|
579 |
( aux false ((id,machine_n)::prefix) machine_n ) |
|
580 | 580 |
@ accu |
581 |
) [] m.minstances
|
|
581 |
) [] m.minstances |
|
582 | 582 |
in |
583 | 583 |
aux true [] m |
584 | 584 |
in |
585 | 585 |
|
586 | 586 |
List.iter (fun m -> |
587 | 587 |
Format.fprintf fmt "; Node %s@." m.mname.node_id; |
588 |
|
|
589 |
let memories_old =
|
|
590 |
List.map (fun (p, v) ->
|
|
588 |
|
|
589 |
let memories_old = |
|
590 |
List.map (fun (p, v) -> |
|
591 | 591 |
let machine = match p with | [] -> m | (_,m')::_ -> m' in |
592 | 592 |
let traces = List.assoc machine machines_traces in |
593 | 593 |
if List.mem_assoc v.var_id traces then |
... | ... | |
596 | 596 |
else |
597 | 597 |
(* We keep the variable as is: we create an expression v *) |
598 | 598 |
p, mkexpr Location.dummy_loc (Expr_ident v.var_id) |
599 |
|
|
600 |
) (compute_mems m)
|
|
599 |
|
|
600 |
) (compute_mems m) |
|
601 | 601 |
in |
602 | 602 |
let memories_next = (* We remove the topest pre in each expression *) |
603 |
List.map
|
|
604 |
(fun (prefix, ee) ->
|
|
605 |
match ee.expr_desc with
|
|
606 |
| Expr_pre e -> prefix, e
|
|
607 |
| _ -> Format.eprintf
|
|
608 |
"Mem Failure: (prefix: %a, eexpr: %a)@.@?"
|
|
609 |
(Utils.fprintf_list ~sep:","
|
|
610 |
(fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id ))
|
|
611 |
(List.rev prefix)
|
|
612 |
Printers.pp_expr ee;
|
|
603 |
List.map |
|
604 |
(fun (prefix, ee) -> |
|
605 |
match ee.expr_desc with |
|
606 |
| Expr_pre e -> prefix, e |
|
607 |
| _ -> Format.eprintf |
|
608 |
"Mem Failure: (prefix: %a, eexpr: %a)@.@?" |
|
609 |
(Utils.fprintf_list ~sep:"," |
|
610 |
(fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id )) |
|
611 |
(List.rev prefix) |
|
612 |
Printers.pp_expr ee; |
|
613 | 613 |
assert false) |
614 | 614 |
memories_old |
615 | 615 |
in |
... | ... | |
645 | 645 |
(Utils.fprintf_list ~sep:" " pp_var) (m.mstep.step_inputs@m.mstep.step_outputs) |
646 | 646 |
(fun fmt -> match memories_old with [] -> () | _ -> fprintf fmt " ") |
647 | 647 |
(Utils.fprintf_list ~sep:" " (fun fmt (prefix,ee) -> fprintf fmt "%a(%a)" pp_prefix_rev prefix Printers.pp_expr ee)) (memories_old@memories_next); |
648 |
Format.pp_print_newline fmt ();
|
|
648 |
Format.pp_print_newline fmt (); |
|
649 | 649 |
) (List.rev machines); |
650 |
|
|
650 |
|
|
651 | 651 |
|
652 | 652 |
(* Local Variables: *) |
653 | 653 |
(* compile-command:"make -C .." *) |
Also available in: Unified diff
Fixed horn backend to make query for properties. More work needed for cex