From 8f4220e08dbb8f96e442f0111cddea844c9f9d46 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?C=C3=A9dric=20Pasteur?= Date: Wed, 28 Jul 2010 12:34:07 +0200 Subject: [PATCH] Made Eupdate dynamic Modifying an array with [ a with [i] = v ] should expected a dynamic (not static) value for i (nothing happens if i is in the wrong range). This is the same behaviour as in Scade and it is useful eg to modify an array in a foldi. --- compiler/heptagon/analysis/causality.ml | 8 ++++++-- compiler/heptagon/analysis/typing.ml | 8 ++++---- compiler/heptagon/hept_printer.ml | 4 ++-- compiler/heptagon/parsing/hept_parser.mly | 2 +- compiler/main/mls2obc.ml | 14 ++++++++------ compiler/minils/analysis/clocking.ml | 4 ++-- compiler/minils/mls_printer.ml | 4 ++-- compiler/minils/transformations/normalize.ml | 5 +++-- test/good/array1.ept | 8 ++++++-- 9 files changed, 34 insertions(+), 23 deletions(-) diff --git a/compiler/heptagon/analysis/causality.ml b/compiler/heptagon/analysis/causality.ml index c59e563..d9aa932 100644 --- a/compiler/heptagon/analysis/causality.ml +++ b/compiler/heptagon/analysis/causality.ml @@ -125,14 +125,18 @@ and apply op e_list = let i3 = typing e3 in cseq t1 (cor i2 i3) | (Eequal | Efun _| Enode _ | Econcat | Eselect_slice - | Eselect_dyn | Eselect _ | Earray_fill), e_list -> + | Eselect_dyn| Eselect _ | Earray_fill), e_list -> ctuplelist (List.map typing e_list) | (Earray | Etuple), e_list -> candlist (List.map typing e_list) - | (Eupdate _ | Efield_update _), [e1;e2] -> + | Efield_update, [e1;e2] -> let t1 = typing e1 in let t2 = typing e2 in cseq t2 t1 + | Eupdate , e1::e_list -> + let t1 = typing e1 in + let t2 = ctuplelist (List.map typing e_list) in + cseq t2 t1 let rec typing_pat = function | Evarpat(x) -> cwrite(x) diff --git a/compiler/heptagon/analysis/typing.ml b/compiler/heptagon/analysis/typing.ml index a35c794..1398109 100644 --- a/compiler/heptagon/analysis/typing.ml +++ b/compiler/heptagon/analysis/typing.ml @@ -714,12 +714,12 @@ and typing_app const_env h op e_list = typing_array_subscript_dyn const_env h idx_list t1 in ty, op, typed_e1::typed_defe::typed_idx_list - | { a_op = Eupdate; a_params = idx_list }, [e1;e2] -> + | { a_op = Eupdate}, e1::e2::idx_list -> let typed_e1, t1 = typing const_env h e1 in - let typed_idx_list, ty = - typing_array_subscript const_env h idx_list t1 in + let ty, typed_idx_list = + typing_array_subscript_dyn const_env h idx_list t1 in let typed_e2 = expect const_env h ty e2 in - t1, { op with a_params = typed_idx_list }, [typed_e1; typed_e2] + t1, op, typed_e1::typed_e2::typed_idx_list | { a_op = Eselect_slice; a_params = [idx1; idx2] }, [e] -> let typed_idx1 = expect_static_exp const_env (Tid Initial.pint) idx1 in diff --git a/compiler/heptagon/hept_printer.ml b/compiler/heptagon/hept_printer.ml index 46eeec6..79a71f6 100644 --- a/compiler/heptagon/hept_printer.ml +++ b/compiler/heptagon/hept_printer.ml @@ -141,11 +141,11 @@ and print_op ff op params e_list = print_list_r print_exp "[" "][" "] default " ff idx_list; print_exp ff defe; fprintf ff ")@]" - | Eupdate, idx_list, [e1;e2] -> + | Eupdate, _, e1::e2::idx_list -> fprintf ff "(@["; print_exp ff e1; fprintf ff " with "; - print_list_r print_static_exp "[" "][" "]" ff idx_list; + print_list_r print_exp "[" "][" "]" ff idx_list; fprintf ff " = "; print_exp ff e2; fprintf ff ")@]" diff --git a/compiler/heptagon/parsing/hept_parser.mly b/compiler/heptagon/parsing/hept_parser.mly index 97df578..5ccecf1 100644 --- a/compiler/heptagon/parsing/hept_parser.mly +++ b/compiler/heptagon/parsing/hept_parser.mly @@ -456,7 +456,7 @@ _exp: | simple_exp DOT indexes DEFAULT exp { mk_call Eselect_dyn ([$1; $5]@$3) } | LBRACKET exp WITH indexes EQUAL exp RBRACKET - { mk_call ~params:$4 Eupdate [$2; $6] } + { mk_call Eupdate ($2::$6::$4) } | simple_exp LBRACKET exp DOUBLE_DOT exp RBRACKET { mk_call ~params:[$3; $5] Eselect_slice [$1] } | exp AROBASE exp diff --git a/compiler/main/mls2obc.ml b/compiler/main/mls2obc.ml index 1a76c1d..eadebfd 100644 --- a/compiler/main/mls2obc.ml +++ b/compiler/main/mls2obc.ml @@ -225,14 +225,16 @@ let rec translate_eq map call_context { Minils.eq_lhs = pat; Minils.eq_rhs = e } v, si, j, (control map ck action) :: s | Minils.Evarpat x, - Minils.Eapp ({ Minils.a_op = Minils.Eupdate; - Minils.a_params = idx }, [e1; e2], _) -> + Minils.Eapp ({ Minils.a_op = Minils.Eupdate }, + e1::e2::idx, _) -> let x = var_from_name map x in - let copy = Aassgn (x, translate map (si, j, s) e1) in - let idx = List.map (fun idx -> mk_exp (Econst idx)) idx in + let bounds = Mls_utils.bounds_list e1.Minils.e_ty in + let idx = List.map (translate map (si, j, s)) idx in let action = Aassgn (lhs_of_idx_list x idx, - translate map (si, j, s) e2) - in + translate map (si, j, s) e2) in + let cond = bound_check_expr idx bounds in + let action = Acase (cond, [ Name "true", mk_block [action] ]) in + let copy = Aassgn (x, translate map (si, j, s) e1) in v, si, j, (control map ck copy) :: (control map ck action) :: s | Minils.Evarpat x, diff --git a/compiler/minils/analysis/clocking.ml b/compiler/minils/analysis/clocking.ml index ac74be9..41e8cff 100644 --- a/compiler/minils/analysis/clocking.ml +++ b/compiler/minils/analysis/clocking.ml @@ -81,9 +81,9 @@ and typing_op op args h e ck = match op, args with | Eselect_dyn, e1::defe::idx -> (* TODO defe not treated ? *) let ct = skeleton ck e1.e_ty in (expect h ct e1; List.iter (expect h ct) idx; ct) - | Eupdate, [e1; e2] -> + | Eupdate, e1::e2::idx -> let ct = skeleton ck e.e_ty - in (expect h (Ck ck) e1; expect h ct e2; ct) + in (expect h (Ck ck) e1; expect h ct e2; List.iter (expect h ct) idx; ct) | Eselect_slice, [e] -> typing h e | Econcat, [e1; e2] -> let ct = skeleton ck e.e_ty diff --git a/compiler/minils/mls_printer.ml b/compiler/minils/mls_printer.ml index f144c8a..db8d9ea 100644 --- a/compiler/minils/mls_printer.ml +++ b/compiler/minils/mls_printer.ml @@ -133,9 +133,9 @@ and print_app ff (app, args) = match app.a_op, app.a_params, args with | Eselect_dyn, _, r::d::e -> fprintf ff "%a%a default %a" print_exp r print_dyn_index e print_exp d - | Eupdate, idx, [e1; e2] -> + | Eupdate, _, e1::e2::idx -> fprintf ff "@[<2>(%a with %a =@ %a)@]" - print_exp e1 print_index idx print_exp e2 + print_exp e1 print_dyn_index idx print_exp e2 | Econcat, _,[e1; e2] -> fprintf ff "@[<2>%a@ @@ %a@]" print_exp e1 print_exp e2 | Elambda(inp, outp, _, eq_list), _, e_list -> diff --git a/compiler/minils/transformations/normalize.ml b/compiler/minils/transformations/normalize.ml index 5aed1cf..d5378a3 100644 --- a/compiler/minils/transformations/normalize.ml +++ b/compiler/minils/transformations/normalize.ml @@ -242,10 +242,11 @@ and translate_app kind context op e_list = let context, idx = translate_list Exp context idx in let context, e2 = translate Exp context e2 in context, e1::e2::idx - | Eupdate, [e1; e2] -> + | Eupdate, e1::e2::idx -> let context, e1 = translate VRef context e1 in + let context, idx = translate_list Exp context idx in let context, e2 = translate Exp context e2 in - context, [e1; e2] + context, e1::e2::idx | Eselect_slice, [e'] -> let context, e' = translate VRef context e' in context, [e'] diff --git a/test/good/array1.ept b/test/good/array1.ept index 09867e6..143ba5d 100644 --- a/test/good/array1.ept +++ b/test/good/array1.ept @@ -6,7 +6,7 @@ let o1 = a @ b; o2 = b @ a; tel -(* + node slicing (a:int^n) returns (u1,u2 : int^3) let u1 = a[0 .. 2]; @@ -20,6 +20,11 @@ let o = [ a with [1] = x ]; tel +node upd_dyn(a:int^m; i:int) returns (o:int^m) +let + o = [ a with [i] = a[0] ]; +tel + node elt_dyn (a:int^m; i:int) returns (o:int^m) var x : int; let @@ -36,4 +41,3 @@ node constant(a,b:int) returns (o:int^4) let o = [a,b,a,b]; tel -*) \ No newline at end of file