Better handling of static arrays
This commit is contained in:
parent
220db42076
commit
073ccc2603
|
@ -103,6 +103,8 @@ type kind = ExtValue | Any
|
||||||
(** Creates an equation and add it to the context if necessary. *)
|
(** Creates an equation and add it to the context if necessary. *)
|
||||||
let add context expected_kind e =
|
let add context expected_kind e =
|
||||||
let up = match e.e_desc, expected_kind with
|
let up = match e.e_desc, expected_kind with
|
||||||
|
(* static arrays should be normalized to simplify code generation *)
|
||||||
|
| Econst { se_desc = Sarray _ }, ExtValue -> true
|
||||||
| (Evar _ | Eapp ({ a_op = Efield }, _, _) | Ewhen _
|
| (Evar _ | Eapp ({ a_op = Efield }, _, _) | Ewhen _
|
||||||
| Eapp ({ a_op = Etuple }, _, _) | Econst _) , ExtValue -> false
|
| Eapp ({ a_op = Etuple }, _, _) | Econst _) , ExtValue -> false
|
||||||
| _ , ExtValue -> true
|
| _ , ExtValue -> true
|
||||||
|
|
|
@ -77,7 +77,7 @@ let array_elt_of_exp idx e =
|
||||||
| Econst ({ se_desc = Sarray_power (c, _) }), Tarray (ty,_) ->
|
| Econst ({ se_desc = Sarray_power (c, _) }), Tarray (ty,_) ->
|
||||||
mk_exp ty (Econst c)
|
mk_exp ty (Econst c)
|
||||||
| _, Tarray (ty,_) ->
|
| _, Tarray (ty,_) ->
|
||||||
mk_pattern_exp ty (Larray(pattern_of_exp e, mk_exp Initial.tint (Epattern idx)))
|
mk_pattern_exp ty (Larray(pattern_of_exp e, idx))
|
||||||
| _ -> internal_error "mls2obc" 2
|
| _ -> internal_error "mls2obc" 2
|
||||||
|
|
||||||
(** Creates the expression that checks that the indices
|
(** Creates the expression that checks that the indices
|
||||||
|
@ -114,14 +114,14 @@ let rec update_array dest src idx_list v = match dest.pat_ty, idx_list with
|
||||||
| Tarray (t, n), idx::idx_list ->
|
| Tarray (t, n), idx::idx_list ->
|
||||||
(*Body of the copy loops*)
|
(*Body of the copy loops*)
|
||||||
let copy i =
|
let copy i =
|
||||||
let src_i = mk_pattern_exp t (Larray (src, i)) in
|
let src_i = array_elt_of_exp i src in
|
||||||
let dest_i = mk_pattern t (Larray (dest, i)) in
|
let dest_i = mk_pattern t (Larray (dest, i)) in
|
||||||
[Aassgn(dest_i, src_i)]
|
[Aassgn(dest_i, src_i)]
|
||||||
in
|
in
|
||||||
(*Copy values < idx*)
|
(*Copy values < idx*)
|
||||||
let a_lower = fresh_for (mk_exp_const_int 0) idx copy in
|
let a_lower = fresh_for (mk_exp_const_int 0) idx copy in
|
||||||
(* Update the correct element*)
|
(* Update the correct element*)
|
||||||
let src_idx = mk_pattern t (Larray (src, idx)) in
|
let src_idx = array_elt_of_exp idx src in
|
||||||
let dest_idx = mk_pattern t (Larray (dest, idx)) in
|
let dest_idx = mk_pattern t (Larray (dest, idx)) in
|
||||||
let a_update = update_array dest_idx src_idx idx_list v in
|
let a_update = update_array dest_idx src_idx idx_list v in
|
||||||
(*Copy values > idx*)
|
(*Copy values > idx*)
|
||||||
|
@ -253,11 +253,10 @@ and translate_act map pat
|
||||||
let a1 =
|
let a1 =
|
||||||
Afor (cpt1d, mk_exp_const_int 0, mk_exp_static_int n1,
|
Afor (cpt1d, mk_exp_const_int 0, mk_exp_static_int n1,
|
||||||
mk_block [Aassgn (mk_pattern t1 (Larray (x, mk_evar_int cpt1)),
|
mk_block [Aassgn (mk_pattern t1 (Larray (x, mk_evar_int cpt1)),
|
||||||
mk_pattern_exp t1 (Larray (pattern_of_exp e1,
|
array_elt_of_exp (mk_evar_int cpt1) e1)] ) in
|
||||||
mk_evar_int cpt1)))] ) in
|
|
||||||
let idx = mk_exp_int (Eop (op_from_string "+",
|
let idx = mk_exp_int (Eop (op_from_string "+",
|
||||||
[ mk_exp_int (Econst n1); mk_evar_int cpt2])) in
|
[ mk_exp_int (Econst n1); mk_evar_int cpt2])) in
|
||||||
let p2 = mk_pattern_exp t2 (Larray (pattern_of_exp e2, mk_evar_int cpt2)) in
|
let p2 = array_elt_of_exp (mk_evar_int cpt2) e2 in
|
||||||
let a2 = Afor (cpt2d, mk_exp_const_int 0, mk_exp_static_int n2,
|
let a2 = Afor (cpt2d, mk_exp_const_int 0, mk_exp_static_int n2,
|
||||||
mk_block [Aassgn (mk_pattern t2 (Larray (x, idx)), p2)] )
|
mk_block [Aassgn (mk_pattern t2 (Larray (x, idx)), p2)] )
|
||||||
in
|
in
|
||||||
|
@ -293,7 +292,7 @@ and translate_act map pat
|
||||||
[ mk_static_int 1; mk_static_int_op (op_from_string "-") [idx2;idx1] ] in
|
[ mk_static_int 1; mk_static_int_op (op_from_string "-") [idx2;idx1] ] in
|
||||||
[ Afor (cptd, mk_exp_const_int 0, mk_exp_static_int bound,
|
[ Afor (cptd, mk_exp_const_int 0, mk_exp_static_int bound,
|
||||||
mk_block [Aassgn (mk_pattern t (Larray (x, mk_evar_int cpt)),
|
mk_block [Aassgn (mk_pattern t (Larray (x, mk_evar_int cpt)),
|
||||||
mk_pattern_exp t (Larray (pattern_of_exp e, idx)))] ) ]
|
array_elt_of_exp idx e)] ) ]
|
||||||
|
|
||||||
| Minils.Evarpat x, Minils.Eapp ({ Minils.a_op = Minils.Eselect_dyn }, e1::e2::idx, _) ->
|
| Minils.Evarpat x, Minils.Eapp ({ Minils.a_op = Minils.Eselect_dyn }, e1::e2::idx, _) ->
|
||||||
let x = var_from_name map x in
|
let x = var_from_name map x in
|
||||||
|
@ -321,7 +320,7 @@ and translate_act map pat
|
||||||
let e1 = translate_extvalue map e1 in
|
let e1 = translate_extvalue map e1 in
|
||||||
let e2 = translate_extvalue map e2 in
|
let e2 = translate_extvalue map e2 in
|
||||||
let cond = bound_check_expr idx bounds in
|
let cond = bound_check_expr idx bounds in
|
||||||
let true_act = update_array x (pattern_of_exp e1) idx e2 in
|
let true_act = update_array x e1 idx e2 in
|
||||||
let false_act = Aassgn (x, e1) in
|
let false_act = Aassgn (x, e1) in
|
||||||
[ mk_ifthenelse cond true_act [false_act] ]
|
[ mk_ifthenelse cond true_act [false_act] ]
|
||||||
|
|
||||||
|
@ -487,7 +486,7 @@ and translate_iterator map call_context it name_list
|
||||||
List.map2 (fun l ty -> mk_pattern ty (Larray (l, mk_evar_int x))) name_list ty_list
|
List.map2 (fun l ty -> mk_pattern ty (Larray (l, mk_evar_int x))) name_list ty_list
|
||||||
in
|
in
|
||||||
let array_of_input c_list =
|
let array_of_input c_list =
|
||||||
List.map (array_elt_of_exp (mk_pattern_int (Lvar x))) c_list in
|
List.map (array_elt_of_exp (mk_evar_int x)) c_list in
|
||||||
match it with
|
match it with
|
||||||
| Minils.Imap ->
|
| Minils.Imap ->
|
||||||
let c_list = array_of_input c_list in
|
let c_list = array_of_input c_list in
|
||||||
|
|
Loading…
Reference in a new issue