Revision 1147e80a
Added by Pierre-Loïc Garoche almost 5 years ago
| src/normalization.ml | ||
|---|---|---|
| 112 | 112 |
expr_tag = Utils.new_tag (); |
| 113 | 113 |
expr_desc = Expr_tuple (List.map expr_of_vdecl locals) } |
| 114 | 114 |
|
| 115 |
let unfold_offsets e offsets = |
|
| 116 |
let add_offset e d = |
|
| 117 |
(*Format.eprintf "add_offset %a(%a) %a @." Printers.pp_expr e Types.print_ty e.expr_type Dimension.pp_dimension d; |
|
| 118 |
let res = *) |
|
| 119 |
{ e with
|
|
| 120 |
expr_tag = Utils.new_tag (); |
|
| 121 |
expr_loc = d.Dimension.dim_loc; |
|
| 122 |
expr_type = Types.array_element_type e.expr_type; |
|
| 123 |
expr_desc = Expr_access (e, d) } |
|
| 124 |
(*in (Format.eprintf "= %a @." Printers.pp_expr res; res) *) |
|
| 125 |
in |
|
| 126 |
List.fold_left add_offset e offsets |
|
| 127 |
|
|
| 115 |
|
|
| 128 | 116 |
(* IS IT USED ? TODO |
| 129 | 117 |
(* Create an alias for [expr], if none exists yet *) |
| 130 | 118 |
let mk_expr_alias (parentid, vars) (defs, vars) expr = |
| ... | ... | |
| 147 | 135 |
*) |
| 148 | 136 |
|
| 149 | 137 |
(* Create an alias for [expr], if [expr] is not already an alias (i.e. an ident) |
| 150 |
and [opt] is true *) |
|
| 138 |
and [opt] is true |
|
| 139 |
|
|
| 140 |
|
|
| 141 |
*) |
|
| 151 | 142 |
let mk_expr_alias_opt opt norm_ctx (defs, vars) expr = |
| 152 | 143 |
if !debug then |
| 153 | 144 |
Log.report ~plugin:"normalization" ~level:2 |
| ... | ... | |
| 189 | 180 |
else |
| 190 | 181 |
(defs, vars), expr |
| 191 | 182 |
|
| 183 |
(* Similar fonctions for dimensions *) |
|
| 184 |
let mk_dim_alias opt norm_ctx (defs, vars) dim = |
|
| 185 |
match dim.Dimension.dim_desc with |
|
| 186 |
| Dimension.Dbool _ | Dint _ |
|
| 187 |
| Dident _ -> (defs, vars), dim (* Keep the same *) |
|
| 188 |
| _ when opt -> (* Cast to expression, normalizing *) |
|
| 189 |
let e = expr_of_dimension dim in |
|
| 190 |
let defvars, e = mk_expr_alias_opt true norm_ctx (defs, vars) e in |
|
| 191 |
defvars, dimension_of_expr e |
|
| 192 |
|
|
| 193 |
| _ -> (defs, vars), dim (* Keep the same *) |
|
| 194 |
|
|
| 195 |
|
|
| 196 |
let unfold_offsets norm_ctx defvars e offsets = |
|
| 197 |
let add_offset (defvars, e) d = |
|
| 198 |
(*Format.eprintf "add_offset %a(%a) %a @." Printers.pp_expr e Types.print_ty e.expr_type Dimension.pp_dimension d; *) |
|
| 199 |
let defvars, d = mk_dim_alias !params.force_alias_internal_fun norm_ctx defvars d in |
|
| 200 |
let new_e = |
|
| 201 |
{ e with
|
|
| 202 |
expr_tag = Utils.new_tag (); |
|
| 203 |
expr_loc = d.Dimension.dim_loc; |
|
| 204 |
expr_type = Types.array_element_type e.expr_type; |
|
| 205 |
expr_desc = Expr_access (e, d) } |
|
| 206 |
in |
|
| 207 |
defvars, new_e |
|
| 208 |
(*in (Format.eprintf "= %a @." Printers.pp_expr res; res) *) |
|
| 209 |
in |
|
| 210 |
List.fold_left add_offset (defvars, e) offsets |
|
| 211 |
|
|
| 212 |
|
|
| 192 | 213 |
(* Create a (normalized) expression from [ref_e], |
| 193 | 214 |
replacing description with [norm_d], |
| 194 | 215 |
taking propagated [offsets] into account |
| ... | ... | |
| 210 | 231 |
) elist (defvars, []) |
| 211 | 232 |
|
| 212 | 233 |
let rec normalize_expr ?(alias=true) ?(alias_basic=false) norm_ctx offsets defvars expr = |
| 213 |
(*Format.eprintf "normalize %B %a:%a [%a]@." alias Printers.pp_expr expr Types.print_ty expr.expr_type (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*)
|
|
| 234 |
(* Format.eprintf "normalize %B %a:%a [%a]@." alias Printers.pp_expr expr Types.print_ty expr.expr_type (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets; *)
|
|
| 214 | 235 |
match expr.expr_desc with |
| 215 | 236 |
| Expr_const _ |
| 216 |
| Expr_ident _ -> defvars, unfold_offsets expr offsets |
|
| 237 |
| Expr_ident _ -> |
|
| 238 |
unfold_offsets norm_ctx defvars expr offsets |
|
| 217 | 239 |
| Expr_array elist -> |
| 218 | 240 |
let defvars, norm_elist = normalize_list alias norm_ctx offsets (fun _ -> normalize_array_expr ~alias:true) defvars elist in |
| 219 | 241 |
let norm_expr = mk_norm_expr offsets expr (Expr_array norm_elist) in |
| ... | ... | |
| 225 | 247 |
| Expr_power (e1, d) -> |
| 226 | 248 |
normalize_expr ~alias:alias norm_ctx (List.tl offsets) defvars e1 |
| 227 | 249 |
| Expr_access (e1, d) -> |
| 228 |
normalize_expr ~alias:alias norm_ctx (d::offsets) defvars e1 |
|
| 250 |
normalize_expr ~alias:alias norm_ctx (d::offsets) defvars e1 |
|
| 251 |
|
|
| 229 | 252 |
| Expr_tuple elist -> |
| 230 | 253 |
let defvars, norm_elist = |
| 231 | 254 |
normalize_list alias norm_ctx offsets (fun alias -> normalize_expr ~alias:alias ~alias_basic:false) defvars elist in |
| 232 | 255 |
defvars, mk_norm_expr offsets expr (Expr_tuple norm_elist) |
| 233 | 256 |
| Expr_appl (id, args, None) |
| 234 | 257 |
when Basic_library.is_homomorphic_fun id |
| 235 |
&& Types.is_array_type expr.expr_type -> |
|
| 258 |
&& Types.is_array_type expr.expr_type ->
|
|
| 236 | 259 |
let defvars, norm_args = |
| 237 | 260 |
normalize_list |
| 238 | 261 |
alias |
| ... | ... | |
| 330 | 353 |
| _ -> normalize_expr ~alias:alias norm_ctx offsets defvars expr |
| 331 | 354 |
|
| 332 | 355 |
and normalize_cond_expr ?(alias=true) norm_ctx offsets defvars expr = |
| 333 |
(*Format.eprintf "normalize_cond %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*)
|
|
| 356 |
(* Format.eprintf "normalize_cond %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets; *)
|
|
| 334 | 357 |
match expr.expr_desc with |
| 335 | 358 |
| Expr_access (e1, d) -> |
| 336 | 359 |
normalize_cond_expr ~alias:alias norm_ctx (d::offsets) defvars e1 |
Also available in: Unified diff
Array access: solved issues in C backend when basic operations in array access dimensions. Also better handling in EMF, ie further normalization through new equations