Revision 44ce4da8
Added by Pierre-Loïc Garoche over 6 years ago
| src/backends/Horn/horn_backend_printers.ml | ||
|---|---|---|
| 46 | 46 |
| Const_tag t -> pp_horn_tag fmt t |
| 47 | 47 |
| _ -> assert false |
| 48 | 48 |
|
| 49 |
let rec get_type_cst c = |
|
| 50 |
match c with |
|
| 51 |
| Const_int(n) -> new_ty Tint |
|
| 52 |
| Const_real _ -> new_ty Treal |
|
| 53 |
(* | Const_float _ -> new_ty Treal *) |
|
| 54 |
| Const_array(l) -> new_ty (Tarray(Dimension.mkdim_int (Location.dummy_loc) (List.length l), get_type_cst (List.hd l))) |
|
| 55 |
| Const_tag(tag) -> new_ty Tbool |
|
| 56 |
| Const_string(str) -> assert false(* used only for annotations *) |
|
| 57 |
| Const_struct(l) -> new_ty (Tstruct(List.map (fun (label, t) -> (label, get_type_cst t)) l)) |
|
| 58 |
|
|
| 49 |
(* PL comment 2017/01/03: Useless code, the function existed before in typing.ml *) |
|
| 50 |
(* let rec get_type_cst c = *) |
|
| 51 |
(* match c with *) |
|
| 52 |
(* | Const_int(n) -> new_ty Tint *) |
|
| 53 |
(* | Const_real _ -> new_ty Treal *) |
|
| 54 |
(* (\* | Const_float _ -> new_ty Treal *\) *) |
|
| 55 |
(* | Const_array(l) -> new_ty (Tarray(Dimension.mkdim_int (Location.dummy_loc) (List.length l), *) |
|
| 56 |
(* get_type_cst (List.hd l))) *) |
|
| 57 |
(* | Const_tag(tag) -> new_ty Tbool *) |
|
| 58 |
(* | Const_string(str) -> assert false(\* used only for annotations *\) *) |
|
| 59 |
(* | Const_struct(l) -> new_ty (Tstruct(List.map (fun (label, t) -> (label, get_type_cst t)) l)) *) |
|
| 60 |
|
|
| 61 |
(* PL comment 2017/01/03: the following function get_type seems useless to me: it looks like computing the type of a machine code expression v while v.value_type should contain this information. The code is kept for the moment in case I missed something *) |
|
| 62 |
|
|
| 63 |
(* |
|
| 59 | 64 |
let rec get_type v = |
| 60 | 65 |
match v with |
| 61 |
| Cst c -> get_type_cst c
|
|
| 66 |
| Cst c -> Typing.type_const Location.dummy_loc c (* get_type_cst c*)
|
|
| 62 | 67 |
| Access(tab, index) -> begin |
| 63 | 68 |
let rec remove_link ltype = |
| 64 | 69 |
match (dynamic_type ltype).tdesc with |
| ... | ... | |
| 85 | 90 |
(List.length l), |
| 86 | 91 |
get_type (List.hd l))) |
| 87 | 92 |
| _ -> assert false |
| 93 |
*) |
|
| 88 | 94 |
|
| 89 |
|
|
| 90 |
let rec default_val fmt t = |
|
| 95 |
(* Default value for each type, used when building arrays. Eg integer array |
|
| 96 |
[2;7] is defined as (store (store (0) 1 7) 0 2) where 0 is this default value |
|
| 97 |
for the type integer (arrays). |
|
| 98 |
*) |
|
| 99 |
let rec pp_default_val fmt t = |
|
| 91 | 100 |
match (dynamic_type t).tdesc with |
| 92 | 101 |
| Tint -> fprintf fmt "0" |
| 93 | 102 |
| Treal -> fprintf fmt "0" |
| 94 | 103 |
| Tbool -> fprintf fmt "true" |
| 95 |
| Tarray(dim, l) -> let valt = array_element_type t in |
|
| 96 |
fprintf fmt "((as const (Array Int "; |
|
| 97 |
begin try |
|
| 98 |
pp_type fmt valt |
|
| 99 |
with |
|
| 100 |
| _ -> fprintf fmt "failed"; end; |
|
| 101 |
fprintf fmt ")) "; |
|
| 102 |
begin try |
|
| 103 |
default_val fmt valt |
|
| 104 |
with |
|
| 105 |
| _ -> fprintf fmt "failed"; end; |
|
| 106 |
fprintf fmt ")" |
|
| 104 |
| Tarray(dim, l) -> (* TODO PL: this strange code has to be (heavily) checked *) |
|
| 105 |
let valt = array_element_type t in |
|
| 106 |
fprintf fmt "((as const (Array Int %a)) %a)" |
|
| 107 |
pp_type valt |
|
| 108 |
pp_default_val valt |
|
| 107 | 109 |
| Tstruct(l) -> assert false |
| 108 | 110 |
| Ttuple(l) -> assert false |
| 109 | 111 |
|_ -> assert false |
| ... | ... | |
| 115 | 117 |
*) |
| 116 | 118 |
let rec pp_horn_val ?(is_lhs=false) self pp_var fmt v = |
| 117 | 119 |
match v.value_desc with |
| 118 |
| Cst c -> pp_horn_const fmt c |
|
| 119 |
| Array initlist -> (*Format.fprintf err_formatter "init %a" (pp_horn_val ~is_lhs:is_lhs self pp_var) (List.hd initlist);*) |
|
| 120 |
let rec print tab x = |
|
| 121 |
match tab with |
|
| 122 |
| [] -> default_val fmt (get_type v)(*fprintf fmt "YAY"*) |
|
| 123 |
| h::t -> fprintf fmt "(store "; print t (x+1); fprintf fmt " %i " x; pp_horn_val ~is_lhs:is_lhs self pp_var fmt h; fprintf fmt ")" |
|
| 124 |
in |
|
| 125 |
print initlist 0 |
|
| 126 |
| Access(tab,index) -> fprintf fmt "(select "; pp_horn_val ~is_lhs:is_lhs self pp_var fmt tab; fprintf fmt " "; pp_horn_val ~is_lhs:is_lhs self pp_var fmt index; fprintf fmt ")" |
|
| 127 |
| Power (v, n) -> assert false |
|
| 128 |
| LocalVar v -> pp_var fmt (rename_machine self v) |
|
| 129 |
| StateVar v -> |
|
| 130 |
if Types.is_array_type v.var_type |
|
| 131 |
then begin assert false; eprintf "toto called\n";fprintf fmt "TOTO" end |
|
| 132 |
else pp_var fmt (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v)) |
|
| 133 |
| Fun (n, vl) -> fprintf fmt "%a" (Basic_library.pp_horn n (pp_horn_val self pp_var)) vl |
|
| 120 |
| Cst c -> pp_horn_const fmt c |
|
| 121 |
|
|
| 122 |
(* Code specific for arrays *) |
|
| 123 |
| Array il -> |
|
| 124 |
(* An array definition: |
|
| 125 |
(store ( |
|
| 126 |
... |
|
| 127 |
(store ( |
|
| 128 |
store ( |
|
| 129 |
default_val |
|
| 130 |
) |
|
| 131 |
idx_n val_n |
|
| 132 |
) |
|
| 133 |
idx_n-1 val_n-1) |
|
| 134 |
... |
|
| 135 |
idx_1 val_1 |
|
| 136 |
) *) |
|
| 137 |
let rec print fmt (tab, x) = |
|
| 138 |
match tab with |
|
| 139 |
| [] -> pp_default_val fmt v.value_type(* (get_type v) *) |
|
| 140 |
| h::t -> |
|
| 141 |
fprintf fmt "(store %a %i %a)" |
|
| 142 |
print (t, (x+1)) |
|
| 143 |
x |
|
| 144 |
(pp_horn_val ~is_lhs:is_lhs self pp_var) h |
|
| 145 |
in |
|
| 146 |
print fmt (il, 0) |
|
| 147 |
|
|
| 148 |
| Access(tab,index) -> |
|
| 149 |
fprintf fmt "(select %a %a)" |
|
| 150 |
(pp_horn_val ~is_lhs:is_lhs self pp_var) tab |
|
| 151 |
(pp_horn_val ~is_lhs:is_lhs self pp_var) index |
|
| 152 |
|
|
| 153 |
(* Code specific for arrays *) |
|
| 154 |
|
|
| 155 |
| Power (v, n) -> assert false |
|
| 156 |
| LocalVar v -> pp_var fmt (rename_machine self v) |
|
| 157 |
| StateVar v -> |
|
| 158 |
if Types.is_array_type v.var_type |
|
| 159 |
then assert false |
|
| 160 |
else pp_var fmt (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v)) |
|
| 161 |
| Fun (n, vl) -> fprintf fmt "%a" (Basic_library.pp_horn n (pp_horn_val self pp_var)) vl |
|
| 134 | 162 |
|
| 135 | 163 |
(* Prints a [value] indexed by the suffix list [loop_vars] *) |
| 136 | 164 |
let rec pp_value_suffix self pp_value fmt value = |
Also available in: Unified diff
Solved some issues with commited code (like it doesn't compile). The code was written by Teme's student and
- did not rely on existing typing.ml function
- used strange fprintf code
Code was refactored but old stuff kept in comment just in case. Will have to be cleaned at some point.