Ported Mls2Obc
This commit is contained in:
Cédric Pasteur
parent
b5fbfad315
commit
4dc345bf8a
3 changed files with 463 additions and 542 deletions
126
minils/minils.ml
126
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
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
}
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -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 "@[<v>";
|
||||
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 "@[<v 1>{";
|
||||
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 "]@]"
|
||||
|
|
|
|||
Loading…
Reference in a new issue