Revision 822f31e1
Added by Teme Kahsai about 8 years ago
| src/backends/Horn/horn_backend_printers.ml | ||
|---|---|---|
| 42 | 42 |
let rec pp_horn_const fmt c = |
| 43 | 43 |
match c with |
| 44 | 44 |
| Const_int i -> pp_print_int fmt i |
| 45 |
| Const_real r -> pp_print_string fmt r |
|
| 46 |
| Const_float r -> pp_print_float fmt r |
|
| 45 |
| Const_real (_,_,s) -> pp_print_string fmt s |
|
| 47 | 46 |
| Const_tag t -> pp_horn_tag fmt t |
| 48 | 47 |
| _ -> assert false |
| 49 | 48 |
|
| ... | ... | |
| 52 | 51 |
but an offset suffix may be added for array variables |
| 53 | 52 |
*) |
| 54 | 53 |
let rec pp_horn_val ?(is_lhs=false) self pp_var fmt v = |
| 55 |
match v with |
|
| 54 |
match v.value_desc with
|
|
| 56 | 55 |
| Cst c -> pp_horn_const fmt c |
| 57 | 56 |
| Array _ |
| 58 | 57 |
| Access _ -> assert false (* no arrays *) |
| ... | ... | |
| 66 | 65 |
|
| 67 | 66 |
(* Prints a [value] indexed by the suffix list [loop_vars] *) |
| 68 | 67 |
let rec pp_value_suffix self pp_value fmt value = |
| 69 |
match value with |
|
| 68 |
match value.value_desc with
|
|
| 70 | 69 |
| Fun (n, vl) -> |
| 71 | 70 |
Basic_library.pp_horn n (pp_value_suffix self pp_value) fmt vl |
| 72 | 71 |
| _ -> |
| ... | ... | |
| 78 | 77 |
- [value]: assigned value |
| 79 | 78 |
- [pp_var]: printer for variables |
| 80 | 79 |
*) |
| 81 |
let pp_assign m pp_var fmt var_type var_name value =
|
|
| 80 |
let pp_assign m pp_var fmt var_name value = |
|
| 82 | 81 |
let self = m.mname.node_id in |
| 83 | 82 |
fprintf fmt "(= %a %a)" |
| 84 | 83 |
(pp_horn_val ~is_lhs:true self pp_var) var_name |
| ... | ... | |
| 157 | 156 |
| "_arrow", [i1; i2], [o], [mem_m], [mem_x] -> begin |
| 158 | 157 |
fprintf fmt "@[<v 5>(and "; |
| 159 | 158 |
fprintf fmt "(= %a (ite %a %a %a))" |
| 160 |
(pp_horn_val ~is_lhs:true self (pp_horn_var m)) (LocalVar o) (* output var *)
|
|
| 159 |
(pp_horn_val ~is_lhs:true self (pp_horn_var m)) (mk_val (LocalVar o) o.var_type) (* output var *)
|
|
| 161 | 160 |
(pp_horn_var m) mem_m |
| 162 | 161 |
(pp_horn_val self (pp_horn_var m)) i1 |
| 163 | 162 |
(pp_horn_val self (pp_horn_var m)) i2 |
| ... | ... | |
| 173 | 172 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m))) inputs |
| 174 | 173 |
(Utils.pp_final_char_if_non_empty "@ " inputs) |
| 175 | 174 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m))) |
| 176 |
(List.map (fun v -> LocalVar v) outputs)
|
|
| 175 |
(List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)
|
|
| 177 | 176 |
(Utils.pp_final_char_if_non_empty "@ " outputs) |
| 178 | 177 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (mid_mems@next_mems) |
| 179 | 178 |
|
| ... | ... | |
| 187 | 186 |
inputs |
| 188 | 187 |
(Utils.pp_final_char_if_non_empty "@ " inputs) |
| 189 | 188 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m))) |
| 190 |
(List.map (fun v -> LocalVar v) outputs)
|
|
| 189 |
(List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)
|
|
| 191 | 190 |
) |
| 192 | 191 |
|
| 193 | 192 |
|
| 194 | 193 |
(* Print the instruction and update the set of reset instances *) |
| 195 | 194 |
let rec pp_machine_instr machines reset_instances (m: machine_t) fmt instr : ident list = |
| 196 | 195 |
match instr with |
| 196 |
| MComment _ -> reset_instances |
|
| 197 | 197 |
| MNoReset i -> (* we assign middle_mem with mem_m. And declare i as reset *) |
| 198 | 198 |
pp_no_reset machines m fmt i; |
| 199 | 199 |
i::reset_instances |
| ... | ... | |
| 203 | 203 |
| MLocalAssign (i,v) -> |
| 204 | 204 |
pp_assign |
| 205 | 205 |
m (pp_horn_var m) fmt |
| 206 |
i.var_type (LocalVar i) v;
|
|
| 206 |
(mk_val (LocalVar i) i.var_type) v;
|
|
| 207 | 207 |
reset_instances |
| 208 | 208 |
| MStateAssign (i,v) -> |
| 209 | 209 |
pp_assign |
| 210 | 210 |
m (pp_horn_var m) fmt |
| 211 |
i.var_type (StateVar i) v;
|
|
| 211 |
(mk_val (StateVar i) i.var_type) v;
|
|
| 212 | 212 |
reset_instances |
| 213 |
| MStep ([i0], i, vl) when Basic_library.is_internal_fun i -> |
|
| 213 |
| MStep ([i0], i, vl) when Basic_library.is_internal_fun i (List.map (fun v -> v.value_type) vl) ->
|
|
| 214 | 214 |
assert false (* This should not happen anymore *) |
| 215 | 215 |
| MStep (il, i, vl) -> |
| 216 | 216 |
(* if reset instance, just print the call over mem_m , otherwise declare mem_m = |
Also available in: Unified diff
updating to onera version 30f766a:2016-12-04