From 4dc345bf8a2d913c5ae51eebd65b3c9993f8bad4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?C=C3=A9dric=20Pasteur?= Date: Fri, 18 Jun 2010 10:30:23 +0200 Subject: [PATCH] Ported Mls2Obc --- minils/minils.ml | 126 ++---- minils/sequential/mls2obc.ml | 827 +++++++++++++++++------------------ minils/sequential/obc.ml | 52 +-- 3 files changed, 463 insertions(+), 542 deletions(-) diff --git a/minils/minils.ml b/minils/minils.ml index 1d42afc..d4b202b 100644 --- a/minils/minils.ml +++ b/minils/minils.ml @@ -147,6 +147,8 @@ type program = let mk_exp ?(exp_ty = Tprod []) ?(clock = Cbase) ?(loc = no_location) desc = { e_desc = desc; e_ty = exp_ty; e_ck = clock; e_loc = loc } +let mk_equation pat exp = + { eq_lhs = pat; eq_rhs = exp; eq_loc = no_location } let rec size_exp_of_exp e = match e.e_desc with @@ -185,65 +187,68 @@ let is_record_type ty = match ty with Not_found -> false) | _ -> false -(* module Vars = struct + let add x acc = + if List.mem x acc then acc else x :: acc + let rec vars_pat acc = function - | Evarpat(x) -> x :: acc - | Etuplepat(pat_list) -> List.fold_left vars_pat acc pat_list + | Evarpat x -> x :: acc + | Etuplepat pat_list -> List.fold_left vars_pat acc pat_list let rec vars_ck acc = function - | Con(ck, c, n) -> if List.mem (IVar n) acc then acc else (IVar n) :: acc + | Con(ck, c, n) -> add n acc | Cbase | Cvar { contents = Cindex _ } -> acc - | Cvar { contents = Clink ck } -> vars_ck acc ck + | Cvar { contents = Clink ck } -> vars_ck acc ck let rec read is_left acc e = - let add x acc = if List.mem (IVar x) acc then acc else (IVar x) :: acc in let acc = match e.e_desc with | Emerge(x, c_e_list) -> let acc = add x acc in - List.fold_left (fun acc (_, e) -> read is_left acc e) acc c_e_list + List.fold_left (fun acc (_, e) -> read is_left acc e) acc c_e_list | Eifthenelse(e1, e2, e3) -> read is_left (read is_left (read is_left acc e1) e2) e3 | Ewhen(e, c, x) -> let acc = add x acc in - read is_left acc e - | Eop(_, _, e_list) + read is_left acc e | Etuple(e_list) -> List.fold_left (read is_left) acc e_list - | Eapp(_, _, e_list) -> List.fold_left (read is_left) acc e_list - | Eevery(_, _, e_list, x) -> + | Ecall(_, e_list, None) -> + List.fold_left (read is_left) acc e_list + | Ecall(_, e_list, Some x) -> let acc = add x acc in List.fold_left (read is_left) acc e_list | Efby(_, e) -> if is_left then vars_ck acc e.e_ck else read is_left acc e - | Ereset_mem (_, _,res) -> add res acc - | Evar(n) -> add n acc - | Efield({ e_desc = Evar x }, f) -> - let acc = add x acc in - let x = IField(x,f) in - if List.mem x acc then acc else x::acc | Efield(e, _) -> read is_left acc e | Estruct(f_e_list) -> List.fold_left (fun acc (_, e) -> read is_left acc e) acc f_e_list | Econst _ | Econstvar _ -> acc - (*Array operators*) - | Earray e_list -> List.fold_left (read is_left) acc e_list - | Erepeat (_,e) -> read is_left acc e - | Eselect (_,e) -> read is_left acc e - | Eselect_dyn (e_list, _, e1, e2) -> - let acc = List.fold_left (read is_left) acc e_list in - read is_left (read is_left acc e1) e2 - | Eupdate (_, e1, e2) | Efield_update (_, e1, e2) -> - read is_left (read is_left acc e1) e2 - | Eselect_slice (_ , _, e) -> read is_left acc e - | Econcat (e1, e2) -> - read is_left (read is_left acc e1) e2 - | Eiterator (_, _, _, _, e_list, _) -> - List.fold_left (read is_left) acc e_list + | Efield_update (_, e1, e2) -> + read is_left (read is_left acc e1) e2 + (*Array operators*) + | Earray e_list -> List.fold_left (read is_left) acc e_list + | Earray_op op -> read_array_op is_left acc op in vars_ck acc e.e_ck + and read_array_op is_left acc = function + | Erepeat (_,e) -> read is_left acc e + | Eselect (_,e) -> read is_left acc e + | Eselect_dyn (e_list, _, e1, e2) -> + let acc = List.fold_left (read is_left) acc e_list in + read is_left (read is_left acc e1) e2 + | Eupdate (_, e1, e2) -> + read is_left (read is_left acc e1) e2 + | Eselect_slice (_ , _, e) -> read is_left acc e + | Econcat (e1, e2) -> + read is_left (read is_left acc e1) e2 + | Eiterator (_, _, _, e_list, None) -> + List.fold_left (read is_left) acc e_list + | Eiterator (_, _, _, e_list, Some x) -> + let acc = add x acc in + List.fold_left (read is_left) acc e_list + let rec remove x = function | [] -> [] | y :: l -> if x = y then l else y :: remove x l @@ -254,72 +259,35 @@ struct match pat, e.e_desc with | Evarpat(n), Efby(_, e1) -> if is_left - then remove (IVar n) (read is_left [] e1) + then remove n (read is_left [] e1) else read is_left [] e1 | _ -> read is_left [] e - let rec remove_records = function - | [] -> [] - | (IVar x)::l -> (IVar x)::(remove_records l) - | (IField(x,f))::l -> - let l = remove (IVar x) l in - (IField(x,f))::(remove_records l) - - let read_ivars is_left eq = - remove_records (read is_left eq) - - let read is_left eq = - filter_vars (read is_left eq) - let antidep { eq_rhs = e } = match e.e_desc with Efby _ -> true | _ -> false + let clock { eq_rhs = e } = match e.e_desc with | Emerge(_, (_, e) :: _) -> e.e_ck | _ -> e.e_ck + let head ck = let rec headrec ck l = match ck with | Cbase | Cvar { contents = Cindex _ } -> l | Con(ck, c, n) -> headrec ck (n :: l) - | Cvar { contents = Clink ck } -> headrec ck l in - headrec ck [] + | Cvar { contents = Clink ck } -> headrec ck l + in + headrec ck [] - let rec linear_use acc e = - match e.e_desc with - | Emerge(_, c_e_list) -> - List.fold_left (fun acc (_, e) -> linear_use acc e) acc c_e_list - | Eifthenelse(e1, e2, e3) -> - linear_use (linear_use (linear_use acc e1) e2) e3 - | Ewhen(e, _, _) | Efield(e, _) | Efby(_, e) -> linear_use acc e - | Eop(_,_, e_list) - | Etuple(e_list) | Earray e_list - | Eapp(_,_, e_list) | Eiterator (_, _, _, _, e_list, _) - | Eevery(_,_, e_list, _) -> List.fold_left linear_use acc e_list - | Evar(n) -> - (match e.e_linearity with - | At _ -> if List.mem n acc then acc else n :: acc - | _ -> acc - ) - | Estruct(f_e_list) -> - List.fold_left (fun acc (_, e) -> linear_use acc e) acc f_e_list - | Econst _ | Econstvar _ | Ereset_mem (_, _,_) -> acc - (*Array operators*) - | Erepeat (_,e) - | Eselect (_,e) | Eselect_slice (_ , _, e) -> linear_use acc e - | Eselect_dyn (e_list, _, e1, e2) -> - let acc = List.fold_left linear_use acc e_list in - linear_use (linear_use acc e1) e2 - | Eupdate (_, e1, e2) | Efield_update (_, e1, e2) - | Econcat (e1, e2) -> - linear_use (linear_use acc e1) e2 - - let mem_reset { eq_rhs = e } = + (** Returns a list of memory vars (x in x = v fby e) + appearing in an equation. *) + let memory_vars ({ eq_lhs = _; eq_rhs = e } as eq) = match e.e_desc with - | Ereset_mem (y, _, _) -> [y] + | Efby(_, _) -> def [] eq | _ -> [] end -*) + (* (* data-flow dependences. pre-dependences are discarded *) module DataFlowDep = Make diff --git a/minils/sequential/mls2obc.ml b/minils/sequential/mls2obc.ml index 6b30c4c..f4f00e8 100644 --- a/minils/sequential/mls2obc.ml +++ b/minils/sequential/mls2obc.ml @@ -7,496 +7,459 @@ (* *) (**************************************************************************) -(* translation from the source language to the target *) - -(* $Id$ *) - +(* Translation from Minils to Obc. *) open Misc -open Names +open Names open Ident -open Global +open Signature open Obc open Control -open Normalize -open Memalloc -open Interference open Static - -(* merge x (C1 -> (merge y (C2 -> e2)) when C1(x)) *) - -(** Targeted inputs should be marked as passed by reference. *) -let update_targeted_inputs targeting inv = - let rec aux i = function - | [] -> [] - | vd::l -> - let vd = - if List.mem_assoc i targeting then (*input is targeted*) - { vd with v_pass_by_ref = true; } - else (*not targeted, leave it*) - vd - in - vd::(aux (i+1) l) - in - aux 0 inv - -let rec encode_name_params n = function + +let rec encode_name_params n = + function | [] -> n - | p::params -> encode_name_params (n^"__"^(string_of_int p)) params - -let encode_longname_params n params = + | p :: params -> encode_name_params (n ^ ("__" ^ (string_of_int p))) params + +let encode_longname_params n params = match n with - | Name n -> Name (encode_name_params n params) - | Modname { qual = qual; id = id } -> - Modname { qual = qual; id = encode_name_params id params } - -let is_op = function - | Modname { qual = "Pervasives"; id = _ } -> true - | _ -> false - -let op_from_string op = - Modname { qual = "Pervasives"; id = op } - -let rec lhs_of_idx_list e = function - | [] -> e - | idx::l -> Array(lhs_of_idx_list e l, idx) - + | Name n -> Name (encode_name_params n params) + | Modname { qual = qual; id = id } -> + Modname { qual = qual; id = encode_name_params id params; } + +let is_op = function + | Modname { qual = "Pervasives"; id = _ } -> true | _ -> false + +let op_from_string op = Modname { qual = "Pervasives"; id = op; } + +let rec lhs_of_idx_list e = function + | [] -> e | idx :: l -> Array (lhs_of_idx_list e l, idx) + (** Creates the expression that checks that the indices in idx_list are in the bounds. If idx_list=[e1;..;ep] and bounds = [n1;..;np], it returns e1 <= n1 && .. && ep <= np *) let rec bound_check_expr idx_list bounds = - match idx_list, bounds with - | [idx], [n] -> - Op (op_from_string "<", [idx; Const (Cint n)]) - | idx::idx_list, n::bounds -> - Op (op_from_string "&", [Op (op_from_string "<", [idx; Const (Cint n)]); - bound_check_expr idx_list bounds]) - | _, _ -> assert false - -let rec translate_type const_env = function - | Minils.Tbase(btyp) -> translate_base_type const_env btyp - | Minils.Tprod _ -> assert false - -and translate_base_type const_env = function - | Minils.Tint -> Tint - | Minils.Tfloat -> Tfloat - | Minils.Tid(id) -> Tid(id) - | Minils.Tarray(ty, n) -> Tarray (translate_base_type const_env ty, - int_of_size_exp const_env n) - -let rec translate_const const_env = function - | Minils.Cint(v) -> Cint(v) - | Minils.Cfloat(v) -> Cfloat(v) - | Minils.Cconstr(c) -> Cconstr(c) - | Minils.Cconst_array(n,c) -> - Cconst_array(int_of_size_exp const_env n, translate_const const_env c) - -let rec translate_pat map = function - | Minils.Evarpat(x) -> [var_from_name map x] - | Minils.Etuplepat(pat_list) -> - List.fold_right (fun pat acc -> (translate_pat map pat) @ acc) pat_list [] - + match (idx_list, bounds) with + | ([ idx ], [ n ]) -> Op (op_from_string "<", [ idx; Const (Cint n) ]) + | (idx :: idx_list, n :: bounds) -> + Op (op_from_string "&", + [ Op (op_from_string "<", [ idx; Const (Cint n) ]); + bound_check_expr idx_list bounds ]) + | (_, _) -> assert false + +let rec translate_type const_env = + function + | Types.Tid id when id = Initial.pint -> Tint + | Types.Tid id when id = Initial.pfloat -> Tfloat + | Types.Tid id when id = Initial.pbool -> Tbool + | Types.Tid id -> Tid id + | Types.Tarray (ty, n) -> + Tarray (translate_type const_env ty, int_of_size_exp const_env n) + | Types.Tprod ty -> assert false + +let rec translate_const const_env = + function + | Minils.Cint v -> Cint v + | Minils.Cfloat v -> Cfloat v + | Minils.Cconstr c -> Cconstr c + | Minils.Carray (n, c) -> + Carray (int_of_size_exp const_env n, translate_const const_env c) + +let rec translate_pat map = + function + | Minils.Evarpat x -> [ var_from_name map x ] + | Minils.Etuplepat pat_list -> + List.fold_right (fun pat acc -> (translate_pat map pat) @ acc) + pat_list [] + (* [translate e = c] *) -let rec translate const_env map (m, si, j, s) ({ Minils.e_desc = desc } as e) = +let rec + translate const_env map (m, si, j, s) (({ Minils.e_desc = desc } as e)) = match desc with - | Minils.Econst(v) -> Const(translate_const const_env v) - | Minils.Evar(n) -> Lhs (var_from_name map n) - | Minils.Econstvar(n) -> - Const (Cint(int_of_size_exp const_env (SVar n))) - | Minils.Eop(n, _, e_list) -> - Op(n, List.map (translate const_env map (m, si, j, s)) e_list) - | Minils.Ewhen(e, _, _) -> translate const_env map (m, si, j, s) (e) - | Minils.Efield(e, field) -> - let e = translate const_env map (m, si, j, s) e in - Lhs (Field(lhs_of_exp e, field)) - | Minils.Estruct(f_e_list) -> - let type_name = - begin match e.Minils.e_ty with - Minils.Tbase(Minils.Tid(name)) -> name - | _ -> assert false - end in - let f_e_list = List.map - (fun (f, e) -> (f, - translate const_env map (m, si, j, s) e)) f_e_list in - Struct(type_name,f_e_list) -(*Array operators*) - | Minils.Earray e_list -> - ArrayLit (List.map (translate const_env map (m, si, j, s)) e_list) - | Minils.Eselect (idx,e) -> - let e = translate const_env map (m, si, j, s) e in - Lhs ( lhs_of_idx_list (lhs_of_exp e) - (List.map (fun e -> Const (Cint (int_of_size_exp const_env e))) idx) ) - | _ -> Minils.Printer.print_exp stdout e; flush stdout; assert false + | Minils.Econst v -> Const (translate_const const_env v) + | Minils.Evar n -> Lhs (var_from_name map n) + | Minils.Econstvar n -> Const (Cint (int_of_size_exp const_env (SVar n))) + | Minils.Ecall ( { Minils.op_name = n; Minils.op_kind = Minils.Eop }, e_list, _) -> + Op (n, List.map (translate const_env map (m, si, j, s)) e_list) + | Minils.Ewhen (e, _, _) -> translate const_env map (m, si, j, s) e + | Minils.Efield (e, field) -> + let e = translate const_env map (m, si, j, s) e + in Lhs (Field (lhs_of_exp e, field)) + | Minils.Estruct f_e_list -> + let type_name = + (match e.Minils.e_ty with + | Types.Tid name -> name + | _ -> assert false) in + let f_e_list = + List.map + (fun (f, e) -> (f, (translate const_env map (m, si, j, s) e))) + f_e_list + in Struct_lit (type_name, f_e_list) + (*Array operators*) + | Minils.Earray e_list -> + Array_lit (List.map (translate const_env map (m, si, j, s)) e_list) + | Minils.Earray_op (Minils.Eselect (idx, e)) -> + let e = translate const_env map (m, si, j, s) e in + let idx_list = + List.map (fun e -> Const (Cint (int_of_size_exp const_env e))) idx + in + Lhs (lhs_of_idx_list (lhs_of_exp e) idx_list) + | _ -> (*Minils_printer.print_exp stdout e; flush stdout;*) assert false (* [translate pat act = si, j, d, s] *) -and translate_act const_env map ((m,_,_,_) as context) pat ({ Minils.e_desc = desc } as act) = +and translate_act const_env map ((m, _, _, _) as context) pat + ({ Minils.e_desc = desc } as act) = match pat, desc with - | Minils.Etuplepat(p_list), Minils.Etuple(act_list) -> - comp (List.map2 (translate_act const_env map context) p_list act_list) - | pat, Minils.Ewhen(e, _, _) -> - translate_act const_env map context pat e - | pat, Minils.Emerge(x, c_act_list) -> - let lhs = var_from_name map x in - (Case(Lhs lhs, translate_c_act_list const_env map context pat c_act_list)) - | Minils.Evarpat(n), _ -> - Assgn(var_from_name map n, translate const_env map context act) - | _ -> - Minils.Printer.print_exp stdout act; - assert false + | Minils.Etuplepat p_list, Minils.Etuple act_list -> + comp (List.map2 (translate_act const_env map context) p_list act_list) + | pat, Minils.Ewhen (e, _, _) -> + translate_act const_env map context pat e + | pat, Minils.Emerge (x, c_act_list) -> + let lhs = var_from_name map x + in + Case (Lhs lhs, + translate_c_act_list const_env map context pat c_act_list) + | Minils.Evarpat n, _ -> + Assgn (var_from_name map n, translate const_env map context act) + | _ -> (*Minils_printer.print_exp stdout act;*) assert false and translate_c_act_list const_env map context pat c_act_list = List.map - (fun (c, act) -> (c, translate_act const_env map context pat act)) + (fun (c, act) -> (c, (translate_act const_env map context pat act))) c_act_list and comp s_list = - List.fold_right (fun s rest -> Comp(s, rest)) s_list Nothing - -let rec translate_eq const_env map { Minils.p_lhs = pat; Minils.p_rhs = e } (m, si, j, s) = - let { Minils.e_desc = desc; Minils.e_ty = ty; Minils.e_ck = ck } = e in - match pat, desc with - | Minils.Evarpat(n), Minils.Efby(opt_c, e) -> - let x = var_from_name map n in + List.fold_right (fun s rest -> Comp (s, rest)) s_list Nothing + +let rec + translate_eq const_env map { Minils.eq_lhs = pat; Minils.eq_rhs = e } + (m, si, j, s) = + let { Minils.e_desc = desc; Minils.e_ty = ty; Minils.e_ck = ck } = e + in + match (pat, desc) with + | Minils.Evarpat n, Minils.Efby (opt_c, e) -> + let x = var_from_name map n in let si = - match opt_c with - | None -> si - | Some(c) -> - if var_name x = n then - (Assgn(x, Const(translate_const const_env c))) :: si - else - si (*this mem is shared, no need to add a reset intruction*) - in + (match opt_c with + | None -> si + | Some c -> (Assgn (x, Const (translate_const const_env c))) :: si) in let ty = translate_type const_env ty in - let m = if var_name x = n then (n, ty) :: m else m in - m, si, j, - (control map ck (Assgn(var_from_name map n, translate const_env map (m, si, j, s) e))) :: s - | pat, Minils.Eapp({ Minils.a_op = n }, params, e_list) -> - let sig_info = (Modules.find_value n).info in + let m = (n, ty) :: m in + let action = + Assgn (var_from_name map n, + translate const_env map (m, si, j, s) e) + in + m, si, j, (control map ck action) :: s + + | pat, Minils.Ecall ({ Minils.op_name = n; Minils.op_params = params; + Minils.op_kind = Minils.Enode }, + e_list, r) -> let name_list = translate_pat map pat in - let name_list = remove_targeted_outputs sig_info.targeting name_list in - let c_list = List.map (translate const_env map (m, si, j, s)) e_list in + let c_list = + List.map (translate const_env map (m, si, j, s)) e_list in let o = gen_symbol () in - let si = (Reinit(o)) :: si in - let params = List.map (int_of_size_exp const_env) params in - let j = (o, encode_longname_params n params, 1) :: j in + let si = (Reinit o) :: si in + let params = List.map (int_of_size_exp const_env) params in + let j = (o, (encode_longname_params n params), 1) :: j in + let action = Step_ap (name_list, Context o, c_list) in let s = - (control map ck (Step_ap(name_list, Context o, c_list))) :: s in - (m, si, j, s) - | pat, Minils.Eevery({ Minils.a_op = n }, params, e_list, r ) -> - let sig_info = (Modules.find_value n).info in - let name_list = translate_pat map pat in - let name_list = remove_targeted_outputs sig_info.targeting name_list in - let c_list = List.map (translate const_env map (m, si, j, s)) e_list in - let o = gen_symbol () in - let si = (Reinit(o)) :: si in - let params = List.map (int_of_size_exp const_env) params in - let j = (o, encode_longname_params n params, 1) :: j in - let s = - (control map (Minils.Con(ck, Name("true"), r)) (Reinit(o))) :: - (control map ck (Step_ap(name_list, Context o, c_list))) :: s in - (m, si, j, s) - | Minils.Etuplepat(p_list), Minils.Etuple(act_list) -> + (match r with + | None -> (control map ck action) :: s + | Some r -> + let ra = + control map (Minils.Con (ck, Name "true", r)) (Reinit o) + in ra :: (control map ck action) :: s + ) + in + m, si, j, s + + | Minils.Etuplepat p_list, Minils.Etuple act_list -> List.fold_right2 - (fun pat e -> translate_eq const_env map { Minils.p_lhs = pat; Minils.p_rhs = e } ) + (fun pat e -> + translate_eq const_env map + (Minils.mk_equation pat e)) p_list act_list (m, si, j, s) - | Minils.Evarpat(x), Minils.Eselect_slice(idx1, idx2, e) -> - let idx1 = int_of_size_exp const_env idx1 in - let idx2 = int_of_size_exp const_env idx2 in - let cpt = Ident.fresh "i" in - let e = translate const_env map (m, si, j, s) e in - let idx = Op(op_from_string "+", [Lhs (Var cpt); Const (Cint idx1)]) in - let action = For(cpt, 0, idx2 - idx1 + 1, - Assgn (Array (var_from_name map x, Lhs (Var cpt)), - Lhs (Array (lhs_of_exp e, idx))) ) in - m, si, j, ((control map ck action)::s) - | Minils.Evarpat(x), Minils.Eselect_dyn (idx, bounds, e1, e2) -> - let x = var_from_name map x in - let e1 = translate const_env map (m, si, j, s) e1 in - let bounds = List.map (int_of_size_exp const_env) bounds in - let idx = List.map (translate const_env map (m, si, j, s)) idx in - let true_act = Assgn(x, Lhs (lhs_of_idx_list (lhs_of_exp e1) idx)) in - let false_act = Assgn(x, translate const_env map (m, si, j, s) e2) in - let cond = bound_check_expr idx bounds in - let action = Case(cond, [Name "true", true_act; Name "false", false_act]) in - m, si, j, ((control map ck action)::s) - | Minils.Evarpat(x), Minils.Eupdate (idx, e1, e2) -> - let x = var_from_name map x in - let copy = Assgn (x, translate const_env map (m, si, j, s) e1) in - let idx = List.map (fun se -> Const (Cint (int_of_size_exp const_env se))) idx in - let action = Assgn (lhs_of_idx_list x idx, - translate const_env map (m, si, j, s) e2) in - m, si, j, ((control map ck copy)::(control map ck action)::s) - | Minils.Evarpat(x), Minils.Erepeat (n, e) -> - let cpt = Ident.fresh "i" in - let action = For (cpt, 0, int_of_size_exp const_env n, - Assgn(Array (var_from_name map x, Lhs (Var cpt)), - translate const_env map (m, si, j, s) e) ) in - m, si, j, ((control map ck action)::s) - | Minils.Evarpat(x), Minils.Econcat(e1, e2) -> - let cpt1 = Ident.fresh "i" in - let cpt2 = Ident.fresh "i" in - let x = var_from_name map x in - (match e1.Minils.e_ty, e2.Minils.e_ty with - | Minils.Tbase(Minils.Tarray(_, n1)), Minils.Tbase(Minils.Tarray(_, n2)) -> - let e1 = translate const_env map (m, si, j, s) e1 in - let e2 = translate const_env map (m, si, j, s) e2 in - let n1 = int_of_size_exp const_env n1 in - let n2 = int_of_size_exp const_env n2 in - let a1 = For(cpt1, 0, n1, - Assgn ( Array(x, Lhs(Var cpt1)), - Lhs (Array(lhs_of_exp e1, Lhs(Var cpt1))) ) ) in - let idx = Op (op_from_string "+", [Const (Cint n1); Lhs (Var cpt2)]) in - let a2 = For(cpt2, 0, n2, - Assgn ( Array(x, idx), - Lhs (Array(lhs_of_exp e2, Lhs(Var cpt2))) ) ) in - m, si, j, (control map ck a1)::(control map ck a2)::s - | _ -> assert false - ) - | pat, Minils.Eiterator(it, f, params, n, e_list, reset) -> - let sig_info = (Modules.find_value f).info in + + | Minils.Evarpat x, Minils.Efield_update (f, e1, e2) -> + let x = var_from_name map x in + let copy = Assgn (x, translate const_env map (m, si, j, s) e1) in + let action = + Assgn (Field (x, f), translate const_env map (m, si, j, s) e2) + in + m, si, j, (control map ck copy) :: (control map ck action) :: s + + | Minils.Evarpat x, + Minils.Earray_op (Minils.Eselect_slice (idx1, idx2, e)) -> + let idx1 = int_of_size_exp const_env idx1 in + let idx2 = int_of_size_exp const_env idx2 in + let cpt = Ident.fresh "i" in + let e = translate const_env map (m, si, j, s) e in + let idx = + Op (op_from_string "+", [ Lhs (Var cpt); Const (Cint idx1) ]) in + let action = + For (cpt, 0, (idx2 - idx1) + 1, + Assgn (Array (var_from_name map x, Lhs (Var cpt)), + Lhs (Array (lhs_of_exp e, idx)))) + in + m, si, j, (control map ck action) :: s + + | Minils.Evarpat x, + Minils.Earray_op (Minils.Eselect_dyn (idx, bounds, e1, e2)) -> + let x = var_from_name map x in + let e1 = translate const_env map (m, si, j, s) e1 in + let bounds = List.map (int_of_size_exp const_env) bounds in + let idx = List.map (translate const_env map (m, si, j, s)) idx in + let true_act = + Assgn (x, Lhs (lhs_of_idx_list (lhs_of_exp e1) idx)) in + let false_act = + Assgn (x, translate const_env map (m, si, j, s) e2) in + let cond = bound_check_expr idx bounds in + let action = + Case (cond, + [ ((Name "true"), true_act); ((Name "false"), false_act) ]) + in + m, si, j, (control map ck action) :: s + + | Minils.Evarpat x, + Minils.Earray_op (Minils.Eupdate (idx, e1, e2)) -> + let x = var_from_name map x in + let copy = Assgn (x, translate const_env map (m, si, j, s) e1) in + let idx = + List.map (fun se -> Const (Cint (int_of_size_exp const_env se))) + idx in + let action = Assgn (lhs_of_idx_list x idx, + translate const_env map (m, si, j, s) e2) + in + m, si, j, (control map ck copy) :: (control map ck action) :: s + + | Minils.Evarpat x, + Minils.Earray_op (Minils.Erepeat (n, e)) -> + let cpt = Ident.fresh "i" in + let action = + For (cpt, 0, int_of_size_exp const_env n, + Assgn (Array (var_from_name map x, Lhs (Var cpt)), + translate const_env map (m, si, j, s) e)) + in + m, si, j, (control map ck action) :: s + + | Minils.Evarpat x, + Minils.Earray_op (Minils.Econcat (e1, e2)) -> + let cpt1 = Ident.fresh "i" in + let cpt2 = Ident.fresh "i" in + let x = var_from_name map x + in + (match e1.Minils.e_ty, e2.Minils.e_ty with + | Types.Tarray (_, n1), Types.Tarray (_, n2) -> + let e1 = translate const_env map (m, si, j, s) e1 in + let e2 = translate const_env map (m, si, j, s) e2 in + let n1 = int_of_size_exp const_env n1 in + let n2 = int_of_size_exp const_env n2 in + let a1 = + For (cpt1, 0, n1, + Assgn (Array (x, Lhs (Var cpt1)), + Lhs (Array (lhs_of_exp e1, Lhs (Var cpt1))))) in + let idx = + Op (op_from_string "+", [ Const (Cint n1); Lhs (Var cpt2) ]) in + let a2 = + For (cpt2, 0, n2, + Assgn (Array (x, idx), + Lhs (Array (lhs_of_exp e2, Lhs (Var cpt2))))) + in + m, si, j, + (control map ck a1) :: (control map ck a2) :: s + | _ -> assert false + ) + + | pat, Minils.Earray_op ( + Minils.Eiterator (it, + { Minils.op_name = f; Minils.op_params = params; + Minils.op_kind = k }, + n, e_list, reset)) -> let name_list = translate_pat map pat in - let name_list = remove_targeted_outputs sig_info.targeting name_list in - let c_list = List.map (translate const_env map (m, si, j, s)) e_list in - let o = gen_symbol () in - let n = int_of_size_exp const_env n in - let si = if is_op f then si else (Reinit(o)) :: si in - let params = List.map (int_of_size_exp const_env) params in - let j = (o, encode_longname_params f params, n) :: j in - let x = Ident.fresh "i" in - let action = translate_iterator const_env map it x name_list o sig_info n c_list in - let s = - (match reset with - | None -> (control map ck action)::s - | Some r -> - (control map (Minils.Con(ck, Name("true"), r)) (Reinit(o))) :: - (control map ck action)::s - ) in - m, si, j, s - | Minils.Evarpat(x), Minils.Efield_update (f, e1, e2) -> - let x = var_from_name map x in - let copy = Assgn (x, translate const_env map (m, si, j, s) e1) in - let action = Assgn (Field(x, f), - translate const_env map (m, si, j, s) e2) in - m, si, j, ((control map ck copy)::(control map ck action)::s) - | Minils.Etuplepat [], Minils.Ereset_mem(y, v, res) -> - let h = Initial.ptrue, Assgn(var_from_name map y, Const (translate_const const_env v)) in - let action = Case (Lhs (var_from_name map res), [h]) in - (m, si, j, (control map ck action) :: s) - | pat, _ -> - let action = translate_act const_env map (m, si, j, s) pat e in - (m, si, j, (control map ck action) :: s) + let c_list = + List.map (translate const_env map (m, si, j, s)) e_list in + let o = gen_symbol () in + let n = int_of_size_exp const_env n in + let si = + (match k with + | Minils.Eop -> si + | Minils.Enode -> (Reinit o) :: si) in + let params = List.map (int_of_size_exp const_env) params in + let j = (o, (encode_longname_params f params), n) :: j in + let x = Ident.fresh "i" in + let action = + translate_iterator const_env map it x name_list o n c_list in + let s = + (match reset with + | None -> (control map ck action) :: s + | Some r -> + (control map (Minils.Con (ck, Name "true", r)) (Reinit o)) :: + (control map ck action) :: s + ) + in (m, si, j, s) -and translate_iterator const_env map it x name_list o sig_info n c_list = + | (pat, _) -> + let action = translate_act const_env map (m, si, j, s) pat e + in (m, si, j, ((control map ck action) :: s)) + +and translate_iterator const_env map it x name_list o n c_list = match it with - | Imap -> - let c_list = List.map (fun e -> Lhs (Array(lhs_of_exp e, Lhs (Var x)))) c_list in - let name_list = List.map (fun l -> Array(l, Lhs (Var x))) name_list in - let objn = Array_context (o, Var x) in - For(x, 0, n, - Step_ap (name_list, objn, c_list)) + | Minils.Imap -> + let c_list = + List.map (fun e -> Lhs (Array (lhs_of_exp e, Lhs (Var x)))) c_list in + let name_list = List.map (fun l -> Array (l, Lhs (Var x))) name_list in + let objn = Array_context (o, Var x) in + For (x, 0, n, Step_ap (name_list, objn, c_list)) - | Imapfold -> - let c_list, acc_in = split_last c_list in - let c_list = List.map (fun e -> Lhs (Array(lhs_of_exp e, Lhs (Var x)))) c_list in - let objn = Array_context (o, Var x) in - - let acc_is_targeted = (is_empty name_list) - or (last_element sig_info.inputs).a_pass_by_ref in - if acc_is_targeted then ( - (* no accumulator in output; the accumulator is modified in place *) - let name_list = List.map (fun l -> Array(l, Lhs (Var x))) name_list in - For (x, 0, n, - Step_ap(name_list, objn, c_list@[acc_in])) - ) else ( - (* use the output acc as accumulator*) - let name_list, acc_out = split_last name_list in - let name_list = List.map (fun l -> Array(l, Lhs (Var x))) name_list in - Comp( Assgn(acc_out, acc_in), - For (x, 0, n, - Step_ap(name_list@[acc_out], objn, c_list@[Lhs acc_out])) ) - ) - - | Ifold -> - let c_list, acc_in = split_last c_list in - let c_list = List.map (fun e -> Lhs (Array(lhs_of_exp e, Lhs (Var x)))) c_list in - let objn = Array_context (o, Var x) in - - let acc_is_targeted = (is_empty name_list) in - if acc_is_targeted then ( - (* no accumulator in output; the accumulator is modified in place *) - For (x, 0, n, - Step_ap(name_list, objn, c_list@[acc_in])) - ) else ( - (* use the output acc as accumulator*) - let acc_out = last_element name_list in - Comp( Assgn(acc_out, acc_in), - For (x, 0, n, - Step_ap(name_list, objn, c_list@[Lhs acc_out])) ) - ) + | Minils.Imapfold -> + let (c_list, acc_in) = split_last c_list in + let c_list = + List.map (fun e -> Lhs (Array (lhs_of_exp e, Lhs (Var x)))) c_list in + let objn = Array_context (o, Var x) in + let (name_list, acc_out) = split_last name_list in + let name_list = List.map (fun l -> Array (l, Lhs (Var x))) name_list in + Comp (Assgn (acc_out, acc_in), + For (x, 0, n, + Step_ap (name_list @ [ acc_out ], objn, + c_list @ [ Lhs acc_out ]))) + | Minils.Ifold -> + let (c_list, acc_in) = split_last c_list in + let c_list = + List.map (fun e -> Lhs (Array (lhs_of_exp e, Lhs (Var x)))) c_list in + let objn = Array_context (o, Var x) in + let acc_out = last_element name_list in + Comp (Assgn (acc_out, acc_in), + For (x, 0, n, + Step_ap (name_list, objn, c_list @ [ Lhs acc_out ]))) + let translate_eq_list const_env map act_list = List.fold_right (translate_eq const_env map) act_list ([], [], [], []) - + let remove m d_list = List.filter (fun { Minils.v_name = n } -> not (List.mem_assoc n m)) d_list - + let var_decl l = - List.map (fun (x, t) -> { v_name = x; v_type = t; v_pass_by_ref = false }) l - -let obj_decl l = List.map (fun (x, t, i) -> { obj = x; cls = t; n = i }) l - + List.map (fun (x, t) -> mk_var_dec x t) l + +let obj_decl l = List.map (fun (x, t, i) -> { obj = x; cls = t; size = i; }) l + let translate_var_dec const_env map l = let one_var { Minils.v_name = x; Minils.v_type = t } = - { v_name = x; v_type = translate_base_type const_env t; v_pass_by_ref = false } + mk_var_dec x (translate_type const_env t) in - (* remove unused vars *) - let l = List.filter (fun { Minils.v_name = x } -> - var_name (var_from_name map x) = x) l in List.map one_var l - -let translate_contract const_env map = function - | None -> - [], [], [], [], [], [] - | Some({ Minils.c_eq = eq_list; - Minils.c_local = d_list; - Minils.c_controllables = c_list; - Minils.c_assume = e_a; - Minils.c_enforce = e_c }) -> - let m, si, j, s_list = translate_eq_list const_env map eq_list in + +let translate_contract const_env map = + function + | None -> ([], [], [], [], [], []) + | Some + { + Minils.c_eq = eq_list; + Minils.c_local = d_list; + Minils.c_controllables = c_list; + Minils.c_assume = e_a; + Minils.c_enforce = e_c + } -> + let (m, si, j, s_list) = translate_eq_list const_env map eq_list in let d_list = remove m d_list in let d_list = translate_var_dec const_env map d_list in - let c_list = translate_var_dec const_env map c_list in - m, si, j, s_list, d_list, c_list - -let rec choose_record_field m = function - | [IVar x] -> Var x - | [IField(x,f)] -> Field(var_from_name m x,f) - | (IVar x)::l -> choose_record_field m l - | (IField(x,f))::l -> - if var_name (var_from_name m x) <> x then - choose_record_field m l - else - Field(var_from_name m x,f) - -(** Chooses from a list of vars (with the same color in the interference graph) - the one that will be used to store every other. It can be either an input, - an output or any var if there is no input or output in the list. *) -let choose_representative m inputs outputs mems vars = - let ivar_mem x vars = - match x with - | IVar x -> List.mem x vars - | _ -> false - in - - let inputs = List.filter (fun var -> Minils.ivar_vd_mem var inputs) vars in - let outputs = List.filter (fun var -> Minils.ivar_vd_mem var outputs) vars in - let mems = List.filter (fun var -> ivar_mem var mems) vars in - match inputs, outputs, mems with - | [], [], [] -> choose_record_field m vars - | [], [], (IVar m)::_ -> Mem m - | [IVar vin], [], [] -> Var vin - | [], [IVar vout], [] -> Var vout - | [IVar vin], [IVar vout], [] -> Var vin - | _, _, _ -> - Format.printf "Something is wrong with the coloring : "; - List.iter (fun vd -> Format.printf "%s," (ivar_to_string vd)) vars; - Format.printf "\n Inputs : "; - List.iter (fun vd -> Format.printf "%s," (ivar_to_string vd)) inputs; - Format.printf "\n Outputs : "; - List.iter (fun vd -> Format.printf "%s," (ivar_to_string vd)) outputs; - Format.printf "\n Mem : "; - List.iter (fun vd -> Format.printf "%s," (ivar_to_string vd)) mems; - Format.printf "\n"; - assert false (*something went wrong in the coloring*) - + let c_list = translate_var_dec const_env map c_list + in (m, si, j, s_list, d_list, c_list) + (** Returns a map, mapping variables names to the variables - where they will be stored, as a result of memory allocation. *) -let subst_map_from_coloring subst_lists inputs outputs locals mems = - let rec add_to_map map value = function - | [] -> map - | var::l -> - let m = add_to_map map value l in - (match var with - | IVar x -> Env.add x value m - | _ -> m - ) - in - let map_from_subst_lists m l = - List.fold_left - (fun m (_,l) -> add_to_map m (choose_representative m inputs outputs mems l) l) - m l - in - if !no_mem_alloc then ( - (* Create a map that simply maps each var to itself *) - let m = List.fold_left - (fun m { Minils.v_name = x } -> Env.add x (Var x) m) - Env.empty (inputs @ outputs @ locals) in - List.fold_left (fun m x -> Env.add x (Mem x) m) m mems - ) else ( - let record_lists, other_lists = List.partition - (fun (ty,_) -> Minils.is_record_type ty) subst_lists in - let m = map_from_subst_lists Env.empty record_lists in - map_from_subst_lists m other_lists - ) - -let translate_node_aux const_env - { Minils.n_name = f; Minils.n_input = i_list; Minils.n_output = o_list; - Minils.n_local = d_list; Minils.n_equs = eq_list; - Minils.n_contract = contract ; Minils.n_targeting = targeting; - Minils.n_mem_alloc = mem_alloc; Minils.n_params = params } = - - let mem_vars = List.flatten (List.map InterfRead.memory_vars eq_list) in - let subst_map = subst_map_from_coloring mem_alloc i_list o_list d_list mem_vars in - let m, si, j, s_list = translate_eq_list const_env subst_map eq_list in - let m', si', j', s_list', d_list', c_list = translate_contract const_env subst_map contract in + where they will be stored. *) +let subst_map inputs outputs locals mems = + (* Create a map that simply maps each var to itself *) + let m = + List.fold_left (fun m { Minils.v_name = x } -> Env.add x (Var x) m) + Env.empty (inputs @ outputs @ locals) + in + List.fold_left (fun m x -> Env.add x (Mem x) m) m mems + +let translate_node_aux const_env + { + Minils.n_name = f; + Minils.n_input = i_list; + Minils.n_output = o_list; + Minils.n_local = d_list; + Minils.n_equs = eq_list; + Minils.n_contract = contract; + Minils.n_params = params + } = + let mem_vars = List.flatten (List.map Minils.Vars.memory_vars eq_list) in + let subst_map = subst_map i_list o_list d_list mem_vars in + let (m, si, j, s_list) = translate_eq_list const_env subst_map eq_list in + let (m', si', j', s_list', d_list', c_list) = + translate_contract const_env subst_map contract in let d_list = remove m d_list in let i_list = translate_var_dec const_env subst_map i_list in - let i_list = update_targeted_inputs targeting i_list in let o_list = translate_var_dec const_env subst_map o_list in let d_list = translate_var_dec const_env subst_map d_list in - let s = joinlist (s_list@s_list') in - let m = var_decl (m@m') in - let j = obj_decl (j@j') in - let si = joinlist (si@si') in - let step = { inp = i_list; out = o_list; - local = (d_list@d_list'@c_list); - controllables = c_list; - bd = s } in - { cl_id = f; mem = m; objs = j; reset = si; step = step } - + let s = joinlist (s_list @ s_list') in + let m = var_decl (m @ m') in + let j = obj_decl (j @ j') in + let si = joinlist (si @ si') in + let step = + { + inp = i_list; + out = o_list; + local = d_list @ (d_list' @ c_list); + controllables = c_list; + bd = s; + } + in + { cl_id = f; mem = m; objs = j; reset = si; step = step; } + let build_params_list env params_names params_values = - List.fold_left2 (fun env n v -> NamesEnv.add n (SConst v) env) env params_names params_values - + List.fold_left2 (fun env { p_name = n } v -> NamesEnv.add n (SConst v) env) + env params_names params_values + let translate_node const_env n = let translate_one p = let const_env = build_params_list const_env n.Minils.n_params p in - let c = translate_node_aux const_env n in - { c with cl_id = encode_name_params c.cl_id p; } + let c = translate_node_aux const_env n + in + { c with cl_id = encode_name_params c.cl_id p; } in match n.Minils.n_params_instances with - | [] -> [translate_node_aux const_env n] - | params_lists -> List.map translate_one params_lists - -let translate_ty_def const_env { Minils.t_name = name; Minils.t_desc = tdesc } = - let tdesc = match tdesc with - | Minils.Type_abs -> Type_abs - | Minils.Type_enum(tag_name_list) -> Type_enum(tag_name_list) - | Minils.Type_struct(field_ty_list) -> + | [] -> [ translate_node_aux const_env n ] + | params_lists -> List.map translate_one params_lists + +let translate_ty_def const_env { Minils.t_name = name; Minils.t_desc = tdesc + } = + let tdesc = + match tdesc with + | Minils.Type_abs -> Type_abs + | Minils.Type_enum tag_name_list -> Type_enum tag_name_list + | Minils.Type_struct field_ty_list -> Type_struct - (List.map (fun (f, ty) -> (f, translate_base_type const_env ty)) field_ty_list) - in - { t_name = name; t_desc = tdesc } - + (List.map + (fun { f_name = f; f_type = ty } -> + (f, translate_type const_env ty)) + field_ty_list) + in { t_name = name; t_desc = tdesc; } + let build_const_env cd_list = - List.fold_left (fun env cd -> NamesEnv.add cd.Minils.c_name cd.Minils.c_value env) NamesEnv.empty cd_list - -let program { Minils.p_pragmas = p_pragmas_list; - Minils.p_opened = p_module_list; + List.fold_left + (fun env cd -> NamesEnv.add cd.Minils.c_name cd.Minils.c_value env) + NamesEnv.empty cd_list + +let program { + Minils.p_pragmas = p_pragmas_list; + Minils.p_opened = p_module_list; Minils.p_types = p_type_list; Minils.p_nodes = p_node_list; - Minils.p_consts = p_const_list; } = - let const_env = build_const_env p_const_list in - { o_pragmas = p_pragmas_list; - o_opened = p_module_list; - o_types = List.map (translate_ty_def const_env) p_type_list; - o_defs = List.flatten (List.map (translate_node const_env) p_node_list) } + Minils.p_consts = p_const_list + } = + let const_env = build_const_env p_const_list + in + { + o_pragmas = p_pragmas_list; + o_opened = p_module_list; + o_types = List.map (translate_ty_def const_env) p_type_list; + o_defs = List.flatten (List.map (translate_node const_env) p_node_list); + } + + diff --git a/minils/sequential/obc.ml b/minils/sequential/obc.ml index 1ce6399..f2f7df3 100644 --- a/minils/sequential/obc.ml +++ b/minils/sequential/obc.ml @@ -24,11 +24,11 @@ type op_name = longname type field_name = longname type ty = - | Tint - | Tfloat - | Tbool - | Tid of type_name - | Tarray of ty * int + | Tint + | Tfloat + | Tbool + | Tid of type_name + | Tarray of ty * int type type_dec = { t_name : name; @@ -55,21 +55,21 @@ and exp = | Lhs of lhs | Const of const | Op of op_name * exp list - | Struct of type_name * (field_name * exp) list - | ArrayLit of exp list + | Struct_lit of type_name * (field_name * exp) list + | Array_lit of exp list type obj_call = | Context of obj_name | Array_context of obj_name * lhs type act = - | Assgn of lhs * exp - | Step_ap of lhs list * obj_call * exp list - | Comp of act * act - | Case of exp * (longname * act) list - | For of var_name * int * int * act - | Reinit of obj_name - | Nothing + | Assgn of lhs * exp + | Step_ap of lhs list * obj_call * exp list + | Comp of act * act + | Case of exp * (longname * act) list + | For of var_name * int * int * act + | Reinit of obj_name + | Nothing type var_dec = { v_name : var_name; @@ -104,24 +104,16 @@ type program = o_types : type_dec list; o_defs : class_def list } +let mk_var_dec name ty = + { v_name = name; v_type = ty } + (** [is_scalar_type vd] returns whether the type corresponding to this variable declaration is scalar (ie a type that can be returned by a C function). *) let is_scalar_type vd = match vd.v_type with - | Tint | Tfloat -> true - | Tid name_int when name_int = pint -> true - | Tid name_float when name_float = pfloat -> true - | Tid name_bool when name_bool = pbool -> true - | _ -> false - -let actual_type ty = - match ty with - | Tid(Name("float")) - | Tid(Modname { qual = "Pervasives"; id = "float" }) -> Tfloat - | Tid(Name("int")) - | Tid(Modname { qual = "Pervasives"; id = "int" }) -> Tint - | _ -> ty + | Tint | Tfloat | Tbool -> true + | _ -> false let rec var_name x = match x with @@ -201,8 +193,6 @@ struct fprintf ff "@["; print_ident ff vd.v_name; fprintf ff ": "; - if vd.v_pass_by_ref then - fprintf ff "&"; print_type ff vd.v_type; fprintf ff "@]" @@ -238,14 +228,14 @@ struct | Lhs lhs -> print_lhs ff lhs | Const c -> print_c ff c | Op(op, e_list) -> print_op ff op e_list - | Struct(_,f_e_list) -> + | Struct_lit(_,f_e_list) -> fprintf ff "@[{"; print_list ff (fun ff (field, e) -> print_longname ff field;fprintf ff " = "; print_exp ff e) ";" f_e_list; fprintf ff "}@]" - | ArrayLit e_list -> + | Array_lit e_list -> fprintf ff "@[["; print_list ff print_exp ";" e_list; fprintf ff "]@]"