Revision 1b57e111
Added by Teme Kahsai almost 8 years ago
| src/backends/Horn/horn_backend_printers.ml | ||
|---|---|---|
| 79 | 79 |
*) |
| 80 | 80 |
let pp_assign m pp_var fmt var_name value = |
| 81 | 81 |
let self = m.mname.node_id in |
| 82 |
fprintf fmt "(= %a %a)"
|
|
| 82 |
fprintf fmt "(= %a %a)" |
|
| 83 | 83 |
(pp_horn_val ~is_lhs:true self pp_var) var_name |
| 84 | 84 |
(pp_value_suffix self pp_var) value |
| 85 |
|
|
| 85 |
|
|
| 86 | 86 |
|
| 87 | 87 |
(* In case of no reset call, we define mid_mem = current_mem *) |
| 88 | 88 |
let pp_no_reset machines m fmt i = |
| 89 | 89 |
let (n,_) = List.assoc i m.minstances in |
| 90 | 90 |
let target_machine = List.find (fun m -> m.mname.node_id = (node_name n)) machines in |
| 91 | 91 |
|
| 92 |
let m_list =
|
|
| 92 |
let m_list = |
|
| 93 | 93 |
rename_machine_list |
| 94 | 94 |
(concat m.mname.node_id i) |
| 95 | 95 |
(rename_mid_list (full_memory_vars machines target_machine)) |
| ... | ... | |
| 104 | 104 |
fprintf fmt "(= %a %a)" |
| 105 | 105 |
(pp_horn_var m) mhd |
| 106 | 106 |
(pp_horn_var m) chd |
| 107 |
|
|
| 107 |
|
|
| 108 | 108 |
| _ -> ( |
| 109 | 109 |
fprintf fmt "@[<v 0>(and @[<v 0>"; |
| 110 |
List.iter2 (fun mhd chd ->
|
|
| 110 |
List.iter2 (fun mhd chd -> |
|
| 111 | 111 |
fprintf fmt "(= %a %a)@ " |
| 112 | 112 |
(pp_horn_var m) mhd |
| 113 | 113 |
(pp_horn_var m) chd |
| ... | ... | |
| 120 | 120 |
let pp_instance_reset machines m fmt i = |
| 121 | 121 |
let (n,_) = List.assoc i m.minstances in |
| 122 | 122 |
let target_machine = List.find (fun m -> m.mname.node_id = (node_name n)) machines in |
| 123 |
|
|
| 123 |
|
|
| 124 | 124 |
fprintf fmt "(%a @[<v 0>%a)@]" |
| 125 | 125 |
pp_machine_reset_name (node_name n) |
| 126 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m))
|
|
| 126 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) |
|
| 127 | 127 |
( |
| 128 | 128 |
(rename_machine_list |
| 129 | 129 |
(concat m.mname.node_id i) |
| 130 | 130 |
(rename_current_list (full_memory_vars machines target_machine)) |
| 131 |
)
|
|
| 131 |
) |
|
| 132 | 132 |
@ |
| 133 | 133 |
(rename_machine_list |
| 134 | 134 |
(concat m.mname.node_id i) |
| ... | ... | |
| 146 | 146 |
if not (List.mem i reset_instances) then |
| 147 | 147 |
(* If not, declare mem_m = mem_c *) |
| 148 | 148 |
pp_no_reset machines m fmt i; |
| 149 |
|
|
| 149 |
|
|
| 150 | 150 |
let mems = full_memory_vars machines target_machine in |
| 151 | 151 |
let rename_mems f = rename_machine_list (concat m.mname.node_id i) (f mems) in |
| 152 | 152 |
let mid_mems = rename_mems rename_mid_list in |
| ... | ... | |
| 157 | 157 |
fprintf fmt "@[<v 5>(and "; |
| 158 | 158 |
fprintf fmt "(= %a (ite %a %a %a))" |
| 159 | 159 |
(pp_horn_val ~is_lhs:true self (pp_horn_var m)) (mk_val (LocalVar o) o.var_type) (* output var *) |
| 160 |
(pp_horn_var m) mem_m
|
|
| 160 |
(pp_horn_var m) mem_m |
|
| 161 | 161 |
(pp_horn_val self (pp_horn_var m)) i1 |
| 162 | 162 |
(pp_horn_val self (pp_horn_var m)) i2 |
| 163 | 163 |
; |
| ... | ... | |
| 175 | 175 |
(List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs) |
| 176 | 176 |
(Utils.pp_final_char_if_non_empty "@ " outputs) |
| 177 | 177 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (mid_mems@next_mems) |
| 178 |
|
|
| 178 |
|
|
| 179 | 179 |
end |
| 180 | 180 |
end |
| 181 | 181 |
with Not_found -> ( (* stateless node instance *) |
| ... | ... | |
| 188 | 188 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m))) |
| 189 | 189 |
(List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs) |
| 190 | 190 |
) |
| 191 |
|
|
| 192 |
|
|
| 191 |
|
|
| 192 |
|
|
| 193 | 193 |
(* Print the instruction and update the set of reset instances *) |
| 194 | 194 |
let rec pp_machine_instr machines reset_instances (m: machine_t) fmt instr : ident list = |
| 195 | 195 |
match instr with |
| ... | ... | |
| 230 | 230 |
statement. *) |
| 231 | 231 |
let self = m.mname.node_id in |
| 232 | 232 |
let pp_branch fmt (tag, instrs) = |
| 233 |
fprintf fmt
|
|
| 234 |
"@[<v 3>(or (not (= %a %s))@ "
|
|
| 233 |
fprintf fmt |
|
| 234 |
"@[<v 3>(or (not (= %a %s))@ " |
|
| 235 | 235 |
(*"@[<v 3>(=> (= %a %s)@ "*) (* Issues with some versions of Z3. It |
| 236 | 236 |
seems that => within Horn predicate |
| 237 | 237 |
may cause trouble. I have hard time |
| ... | ... | |
| 244 | 244 |
() (* rs *) |
| 245 | 245 |
in |
| 246 | 246 |
pp_conj pp_branch fmt hl; |
| 247 |
reset_instances
|
|
| 247 |
reset_instances |
|
| 248 | 248 |
|
| 249 |
and pp_machine_instrs machines reset_instances m fmt instrs =
|
|
| 249 |
and pp_machine_instrs machines reset_instances m fmt instrs = |
|
| 250 | 250 |
let ppi rs fmt i = pp_machine_instr machines rs m fmt i in |
| 251 | 251 |
match instrs with |
| 252 |
| [x] -> ppi reset_instances fmt x
|
|
| 252 |
| [x] -> ppi reset_instances fmt x |
|
| 253 | 253 |
| _::_ -> |
| 254 | 254 |
fprintf fmt "(and @[<v 0>"; |
| 255 |
let rs = List.fold_left (fun rs i ->
|
|
| 255 |
let rs = List.fold_left (fun rs i -> |
|
| 256 | 256 |
let rs = ppi rs fmt i in |
| 257 | 257 |
fprintf fmt "@ "; |
| 258 | 258 |
rs |
| 259 | 259 |
) |
| 260 |
reset_instances instrs
|
|
| 260 |
reset_instances instrs |
|
| 261 | 261 |
in |
| 262 | 262 |
fprintf fmt "@])"; |
| 263 | 263 |
rs |
| ... | ... | |
| 269 | 269 |
fprintf fmt "@[<v 5>(and @ "; |
| 270 | 270 |
|
| 271 | 271 |
(* print "x_m = x_c" for each local memory *) |
| 272 |
(Utils.fprintf_list ~sep:"@ " (fun fmt v ->
|
|
| 272 |
(Utils.fprintf_list ~sep:"@ " (fun fmt v -> |
|
| 273 | 273 |
fprintf fmt "(= %a %a)" |
| 274 | 274 |
(pp_horn_var m) (rename_mid v) |
| 275 | 275 |
(pp_horn_var m) (rename_current v) |
| ... | ... | |
| 281 | 281 |
*) |
| 282 | 282 |
(Utils.fprintf_list ~sep:"@ " (fun fmt (id, (n, _)) -> |
| 283 | 283 |
let name = node_name n in |
| 284 |
if name = "_arrow" then (
|
|
| 284 |
if name = "_arrow" then ( |
|
| 285 | 285 |
fprintf fmt "(= %s._arrow._first_m true)" |
| 286 |
(concat m.mname.node_id id)
|
|
| 286 |
(concat m.mname.node_id id) |
|
| 287 | 287 |
) else ( |
| 288 |
let machine_n = get_machine machines name in
|
|
| 289 |
fprintf fmt "(%s_reset @[<hov 0>%a@])"
|
|
| 288 |
let machine_n = get_machine machines name in |
|
| 289 |
fprintf fmt "(%s_reset @[<hov 0>%a@])" |
|
| 290 | 290 |
name |
| 291 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m))
|
|
| 291 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) |
|
| 292 | 292 |
(rename_machine_list (concat m.mname.node_id id) (reset_vars machines machine_n)) |
| 293 | 293 |
) |
| 294 | 294 |
)) fmt m.minstances; |
| ... | ... | |
| 314 | 314 |
else |
| 315 | 315 |
begin |
| 316 | 316 |
fprintf fmt "; %s@." m.mname.node_id; |
| 317 |
|
|
| 317 |
|
|
| 318 | 318 |
(* Printing variables *) |
| 319 | 319 |
Utils.fprintf_list ~sep:"@." pp_decl_var fmt |
| 320 | 320 |
( |
| ... | ... | |
| 358 | 358 |
|
| 359 | 359 |
(* Rule for reset *) |
| 360 | 360 |
fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a @[<v 0>%a)@]@]@.))@.@." |
| 361 |
(pp_machine_reset machines) m
|
|
| 361 |
(pp_machine_reset machines) m |
|
| 362 | 362 |
pp_machine_reset_name m.mname.node_id |
| 363 | 363 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (reset_vars machines m); |
| 364 | 364 |
|
| ... | ... | |
| 373 | 373 |
pp_machine_step_name m.mname.node_id |
| 374 | 374 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (step_vars machines m); |
| 375 | 375 |
end |
| 376 |
| assertsl ->
|
|
| 376 |
| assertsl -> |
|
| 377 | 377 |
begin |
| 378 | 378 |
let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (pp_horn_var m) in |
| 379 | 379 |
(* print_string pp_val; *) |
| 380 | 380 |
fprintf fmt "; with Assertions @."; |
| 381 |
|
|
| 381 |
|
|
| 382 | 382 |
(*Rule for step*) |
| 383 | 383 |
fprintf fmt "@[<v 2>(rule (=> @ (and @ "; |
| 384 | 384 |
ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs); |
| ... | ... | |
| 386 | 386 |
pp_machine_step_name m.mname.node_id |
| 387 | 387 |
(Utils.fprintf_list ~sep:" " (pp_horn_var m)) (step_vars machines m); |
| 388 | 388 |
end |
| 389 |
|
|
| 390 |
|
|
| 389 |
|
|
| 390 |
|
|
| 391 | 391 |
end |
| 392 | 392 |
end |
| 393 | 393 |
|
| 394 | 394 |
|
| 395 |
let mk_flags arity = |
|
| 396 |
let b_range = |
|
| 397 |
let rec range i j = |
|
| 398 |
if i > arity then [] else i :: (range (i+1) j) in |
|
| 399 |
range 2 arity; |
|
| 400 |
in |
|
| 401 |
List.fold_left (fun acc x -> acc ^ " false") "true" b_range |
|
| 402 |
|
|
| 403 |
|
|
| 404 |
(*Get sfunction infos from command line*) |
|
| 405 |
let get_sf_info() = |
|
| 406 |
let splitted = Str.split (Str.regexp "@") !Options.sfunction in |
|
| 407 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. sfunction name: %s@," !Options.sfunction); |
|
| 408 |
let sf_name, flags, arity = match splitted with |
|
| 409 |
[h;flg;par] -> h, flg, par |
|
| 410 |
| _ -> failwith "Wrong Sfunction info" |
|
| 411 |
|
|
| 412 |
in |
|
| 413 |
Log.report ~level:1 (fun fmt -> fprintf fmt "... sf_name: %s@, .. flags: %s@ .. arity: %s@," sf_name flags arity); |
|
| 414 |
sf_name, flags, arity |
|
| 415 |
|
|
| 416 |
|
|
| 417 |
(*a function to print the rules in case we have an s-function*) |
|
| 418 |
let print_sfunction machines fmt m = |
|
| 419 |
if m.mname.node_id = arrow_id then |
|
| 420 |
(* We don't print arrow function *) |
|
| 421 |
() |
|
| 422 |
else |
|
| 423 |
begin |
|
| 424 |
Format.fprintf fmt "; SFUNCTION@."; |
|
| 425 |
Format.fprintf fmt "; %s@." m.mname.node_id; |
|
| 426 |
Format.fprintf fmt "; EndPoint Predicate %s." !Options.sfunction; |
|
| 427 |
|
|
| 428 |
(* Check if there is annotation for s-function *) |
|
| 429 |
if m.mannot != [] then( |
|
| 430 |
Format.fprintf fmt "; @[%a@]@]@\n" (Utils.fprintf_list ~sep:"@ " Printers.pp_s_function) m.mannot; |
|
| 431 |
); |
|
| 432 |
|
|
| 433 |
(* Printing variables *) |
|
| 434 |
Utils.fprintf_list ~sep:"@." pp_decl_var fmt |
|
| 435 |
((step_vars machines m)@ |
|
| 436 |
(rename_machine_list m.mname.node_id m.mstep.step_locals)); |
|
| 437 |
Format.pp_print_newline fmt (); |
|
| 438 |
let sf_name, flags, arity = get_sf_info() in |
|
| 439 |
|
|
| 440 |
if is_stateless m then |
|
| 441 |
begin |
|
| 442 |
(* Declaring single predicate *) |
|
| 443 |
Format.fprintf fmt "(declare-rel %a (%a))@." |
|
| 444 |
pp_machine_stateless_name m.mname.node_id |
|
| 445 |
(Utils.fprintf_list ~sep:" " pp_type) |
|
| 446 |
(List.map (fun v -> v.var_type) (reset_vars machines m)); |
|
| 447 |
Format.pp_print_newline fmt (); |
|
| 448 |
(* Rule for single predicate *) |
|
| 449 |
let str_flags = sf_name ^ " " ^ mk_flags (int_of_string flags) in |
|
| 450 |
Format.fprintf fmt "@[<v 2>(rule (=> @ (%s %a) (%a %a)@]@.))@.@." |
|
| 451 |
str_flags |
|
| 452 |
(Utils.fprintf_list ~sep:" " (pp_horn_var m)) (reset_vars machines m) |
|
| 453 |
pp_machine_stateless_name m.mname.node_id |
|
| 454 |
(Utils.fprintf_list ~sep:" " (pp_horn_var m)) (reset_vars machines m); |
|
| 455 |
end |
|
| 456 |
else |
|
| 457 |
begin |
|
| 458 |
(* Declaring predicate *) |
|
| 459 |
Format.fprintf fmt "(declare-rel %a (%a))@." |
|
| 460 |
pp_machine_reset_name m.mname.node_id |
|
| 461 |
(Utils.fprintf_list ~sep:" " pp_type) |
|
| 462 |
(List.map (fun v -> v.var_type) (inout_vars machines m)); |
|
| 463 |
|
|
| 464 |
Format.fprintf fmt "(declare-rel %a (%a))@." |
|
| 465 |
pp_machine_step_name m.mname.node_id |
|
| 466 |
(Utils.fprintf_list ~sep:" " pp_type) |
|
| 467 |
(List.map (fun v -> v.var_type) (step_vars machines m)); |
|
| 468 |
|
|
| 469 |
Format.pp_print_newline fmt (); |
|
| 470 |
(* Adding assertions *) |
|
| 471 |
match m.mstep.step_asserts with |
|
| 472 |
| [] -> |
|
| 473 |
begin |
|
| 474 |
|
|
| 475 |
(* Rule for step*) |
|
| 476 |
fprintf fmt "@[<v 2>(rule (=> @ "; |
|
| 477 |
ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs); |
|
| 478 |
fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@." |
|
| 479 |
pp_machine_step_name m.mname.node_id |
|
| 480 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (step_vars machines m); |
|
| 481 |
end |
|
| 482 |
| assertsl -> |
|
| 483 |
begin |
|
| 484 |
let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (pp_horn_var m) in |
|
| 485 |
(* print_string pp_val; *) |
|
| 486 |
fprintf fmt "; with Assertions @."; |
|
| 487 |
|
|
| 488 |
(*Rule for step*) |
|
| 489 |
fprintf fmt "@[<v 2>(rule (=> @ (and @ "; |
|
| 490 |
ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs); |
|
| 491 |
fprintf fmt "@. %a)(%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl |
|
| 492 |
pp_machine_step_name m.mname.node_id |
|
| 493 |
(Utils.fprintf_list ~sep:" " (pp_horn_var m)) (step_vars machines m); |
|
| 494 |
end |
|
| 495 |
|
|
| 496 |
end |
|
| 497 |
|
|
| 498 |
end |
|
| 395 | 499 |
(* Local Variables: *) |
| 396 | 500 |
(* compile-command:"make -C ../../.." *) |
| 397 | 501 |
(* End: *) |
Also available in: Unified diff
adding sfunction support