l2lExpandNodes.ml 15.96 KiB
(* Time-stamp: <modified the 22/08/2017 (at 11:30) by Erwan Jahier> *)
open Lxm
open Lic
open AstPredef
let dbg = (Lv6Verbose.get_flag "en")
(* pack useful info into a single struct *)
type local_ctx = {
init_prg : LicPrg.t; (* nodes before expansion *)
curr_prg : LicPrg.t; (* nodes that have already been expanded *)
keep_node_call : Lic.node_key -> bool; (* node calls to expand *)
}
(********************************************************************************)
let new_var label str t c =
let vi = FreshName.var_info str t c in
Lv6Verbose.exe
~flag:dbg
(fun () -> Printf.printf "#EN: new_var[%s](%s)->%s%s'\n"
label str vi.var_name_eff (Lic.string_of_clock (snd c))
);
vi
(********************************************************************************)
let get_locals node =
match node.loclist_eff with
| None -> []
| Some l -> l
let rec (get_node_body : local_ctx -> Lic.node_exp -> Lic.node_body option) =
fun lctx node ->
match node.def_eff with
| ExternLic
| AbstractLic None -> None
| AbstractLic (Some node) -> assert false
| BodyLic node_body -> Some node_body
| MetaOpLic -> None
(********************************************************************************)
(* When expanding a node call such as
x = toto(a when c);
when toto params are (for example) on the base clock, we need to
propagate the substitution between the toto base clock and "on(c)"
; for the toto arguments, it's been done during clock checking ;
but we need to remember this information to substitute the clock
of toto in its local variables.
*)
type new_base = clock
(* to hold the substitution of parameters by arguments *)
module IdMap = Map.Make(struct type t = Lv6Id.t let compare = compare end)
type subst = Lic.var_info IdMap.t
let (add_subst : subst -> Lv6Id.t -> Lic.var_info -> subst) =
fun s id vi -> IdMap.add id vi s
let (subst_in_id : subst -> Lv6Id.t -> Lic.var_info) =
fun s id -> IdMap.find id s
let (subst_in_id_id : subst -> Lv6Id.t -> Lv6Id.t) =
fun s id ->
try (subst_in_id s id).var_name_eff with Not_found -> id
let rec (substitute : subst * new_base ->
Lic.eq_info Lxm.srcflagged -> Lic.eq_info Lxm.srcflagged) = fun s { it = (lhs,ve) ; src = lxm } ->
let lhs = List.map (subst_in_left s ) lhs in
let newve = subst_in_val_exp s ve in
{ it = (lhs,newve) ; src = lxm }
and subst_in_var_info (s,nb) vi =
try
let vi = subst_in_id s vi.var_name_eff in
let id,clk = vi.var_clock_eff in
{ vi with var_clock_eff = subst_in_id_id s id, subst_in_clock (s,nb) clk }
with Not_found ->
assert false (* sno : all i/o have been replace ; fresh locs were created *)
and subst_in_left s left =
match left with
| LeftVarLic(v,lxm) -> LeftVarLic(subst_in_var_info s v,lxm)
| LeftFieldLic(left,id,t) -> LeftFieldLic(subst_in_left s left,id,t)
| LeftArrayLic(left,i, t) -> LeftArrayLic(subst_in_left s left,i, t)
| LeftSliceLic(left,si,t) -> LeftSliceLic(subst_in_left s left,si,t)
and (subst_in_clock : subst * new_base -> clock -> clock) =
fun (s,new_base) clk ->
match clk with
| BaseLic -> new_base
| ClockVar i -> ClockVar i (* sno *)
| On ((cc,cv,ct),clk) ->
On((cc, subst_in_id_id s cv, ct), subst_in_clock (s,new_base) clk)
and (subst_in_val_exp : subst * new_base -> val_exp -> val_exp) =
fun s ve ->
let newve = {
ve with
ve_clk = List.map (subst_in_clock s) ve.ve_clk;
ve_core =
match ve.ve_core with
| CallByPosLic (by_pos_op, vel) ->
let lxm = by_pos_op.src in
let by_pos_op = by_pos_op.it in
let vel = List.map (subst_in_val_exp s) vel in
let by_pos_op = match by_pos_op with
| CONST_REF idl -> CONST_REF idl
| VAR_REF id -> VAR_REF (subst_in_id_id (fst s) id)
| WHEN(clk) -> WHEN(subst_in_clock s clk)
| HAT(i) -> HAT(i)
| PREDEF_CALL _| CALL _ | PRE | ARROW | FBY | CURRENT _ | TUPLE
| ARRAY | CONCAT | STRUCT_ACCESS _ | ARRAY_ACCES _ | ARRAY_SLICE _
| CONST _
-> by_pos_op
in
CallByPosLic(Lxm.flagit by_pos_op lxm, vel)
| CallByNameLic(by_name_op, fl) ->
let fl = List.map (fun (id,ve) -> (id, subst_in_val_exp s ve)) fl in
CallByNameLic(by_name_op, fl)
| Merge(ce,cl) ->
let cl = List.map (fun (id,ve) -> (id, subst_in_val_exp s ve)) cl in
Merge(subst_in_val_exp s ce, cl)
}
in
newve
let (mk_loc_subst:subst -> Lic.var_info list -> Lic.var_info list -> subst) =
fun s l1 l2 ->
let l = List.combine l1 l2 in
List.fold_left
(fun s (v1,v2) -> add_subst s v1.var_name_eff v2)
s l
(********************************************************************************)(** The functions below accumulate
(1) the assertions
(2) the new equations
(3) the fresh variables
The fix-point is performed on nodes.
*)
type acc =
Lic.val_exp srcflagged list (* assertions *)
* (Lic.eq_info srcflagged) list (* equations *)
* Lic.var_info list (* new local vars *)
let (mk_fresh_loc : string -> local_ctx -> var_info -> clock -> var_info) =
fun label lctx v c ->
new_var label ((Lv6Id.to_string v.var_name_eff)) v.var_type_eff (fst v.var_clock_eff, c)
let rec get_new_base c_arg c_par =
match c_arg, c_par with
| _, BaseLic -> c_arg
| On(_,c_arg), On(_,c_par) -> get_new_base c_arg c_par
| _,_ -> assert false (* sno *)
let (mk_input_subst: local_ctx -> Lxm.t -> var_info list ->
Lic.val_exp list -> acc -> subst * acc * new_base option) =
fun lctx lxm vl vel acc ->
assert(List.length vl = List.length vel);
let s, acc, new_base_opt =
List.fold_left2
(fun (s,(a_acc,e_acc,v_acc),nbase_opt) v ve ->
(* we create a new var for each node argument to make sure
that there is no expression in arguments. Is is generally
useless because of the l2lSplit pass, but, well... *)
let carg,cpar = match ve.ve_clk, v.var_clock_eff with
| [c1],(_,c2) -> c1,c2
| _ -> assert false
in
let new_base = get_new_base carg cpar in
let nv = mk_fresh_loc "input" lctx v carg in
let neq = [LeftVarLic(nv,lxm)],ve in
let neq = flagit neq lxm in
let nbase_opt = match nbase_opt with
| None -> Some(new_base)
| Some(b) -> assert(b=new_base); Some(b)
in
add_subst s v.var_name_eff nv,
(a_acc, neq::e_acc, nv::v_acc),
nbase_opt
)
(IdMap.empty, acc, None)
vl
vel
in
s, acc, new_base_opt
(* Create fresh vars if necessary, ie, if we have no trivial left parts *)
let (mk_output_subst : local_ctx -> Lxm.t -> subst -> var_info list -> Lic.left list ->
new_base option-> acc -> subst * acc * new_base) =
fun lctx lxm s vl leftl new_base_opt acc ->
assert(List.length vl = List.length leftl);
let s,acc,new_base_opt =
List.fold_left2
(fun (s,acc,new_base_opt) v left ->
match left with
| LeftVarLic(v2,lxm) -> add_subst s v.var_name_eff v2, acc,new_base_opt
| _ ->
let clk = Lic.clock_of_left left in
let nv = mk_fresh_loc "output" lctx v clk in let nv_id = nv.var_name_eff in
let nve = {
ve_core = CallByPosLic({it=VAR_REF nv_id;src = lxm },[]);
ve_typ = [nv.var_type_eff];
ve_clk = [snd nv.var_clock_eff];
ve_src = lxm
}
in
let neq = [left], nve in
let neq = flagit neq lxm in
(* for equations of the form
x.field = n(...);
we create
- a fresh var "_v"
- define the equation "x.field = _v;"
- create the substition n_output_par/_v
*)
let (aa,ae,av) = acc in
let new_base = get_new_base (Lic.clock_of_left left) (snd v.var_clock_eff) in
let new_base_opt =
match new_base_opt with
| Some x -> assert(x=new_base); Some x
| None -> Some new_base
in
add_subst s v.var_name_eff nv, (aa, neq::ae, nv::av), new_base_opt
)
(s,acc,new_base_opt)
vl
leftl
in
let new_base = match new_base_opt with
| Some x -> x
| None -> assert false (* a node outgth to have at least an input or an output *)
in
s,acc,new_base
let rec (expand_eq : local_ctx * acc -> Lic.eq_info Lxm.srcflagged -> local_ctx * acc) =
fun (lctx, (asserts, eqs, locs)) { src = lxm_eq ; it = eq } ->
match expand_eq_aux lctx eq with
| lctx, None -> lctx, (asserts, { src = lxm_eq ; it = eq }::eqs, locs)
| lctx, Some(nasserts, neqs, nlocs) ->
(lctx,
(List.rev_append nasserts asserts,
List.rev_append neqs eqs,
List.rev_append nlocs locs))
and (expand_eq_aux: local_ctx -> Lic.eq_info -> local_ctx * acc option)=
fun lctx (lhs,ve) ->
match ve.ve_core with
| CallByPosLic( { it = Lic.CALL node_key ; src = lxm }, vel) ->
let lctx, node =
match LicPrg.find_node lctx.curr_prg node_key.it with
| Some node -> lctx, node
| None -> (* node has not been expanded yet: fix point! *)
let raw_node =
match LicPrg.find_node lctx.init_prg node_key.it with
| Some n -> n
| None ->
prerr_string (
"*** "^ (LicDump.string_of_node_key_rec false false node_key.it) ^
" not defined.\n*** Defined nodes are:"^
(String.concat ",\n"
(List.map (fun (nk,_) -> "\""^
LicDump.string_of_node_key_rec false false nk^"\"")
(LicPrg.list_nodes lctx.init_prg)))
);
flush stderr;
assert false
in
expand_node lctx raw_node in
let node = match node.def_eff with
| AbstractLic (Some n) -> { it = n ; src = lxm }
| _ -> flagit node lxm
in
if
(lctx.keep_node_call node.it.node_key_eff)
then
lctx, None
else
(match get_node_body lctx node.it with
| None -> lctx, None
| Some node_body ->
let node_eqs = node_body.eqs_eff
and asserts = node_body.asserts_eff in
let node = node.it in
let node_locs = get_locals node in
let acc = [],[],[] in
(* rename i/o using the calling context *)
let s,acc,new_base = mk_input_subst lctx lxm node.inlist_eff vel acc in
let s,acc,new_base = mk_output_subst lctx lxm s node.outlist_eff
lhs new_base acc in
let rec (substitute_clock : clock -> clock) =
fun c ->
match c with
| BaseLic -> new_base
| ClockVar _ -> new_base (* SNO *)
| On(v,clk) -> On(v, substitute_clock clk)
in
let clks = List.map (fun v -> snd v.var_clock_eff) node_locs in
(* rename locals with fresh names to avoid clashes among locals *)
let fresh_locs = List.map2 (mk_fresh_loc "local" lctx) node_locs clks in
let s = mk_loc_subst s node_locs fresh_locs in
let fresh_locs = (* substitute the new vars in clocks *)
List.map (fun v ->
let id,clk = v.var_clock_eff in
{ v with var_clock_eff =
subst_in_id_id s id, subst_in_clock (s,new_base) clk })
fresh_locs
in
let fresh_locs =
List.map
(fun v ->
let id,clk = v.var_clock_eff in
Lv6Verbose.exe
~flag:dbg
(fun () ->
Printf.printf "#EN: remplace the base clk of %s by '%s'\n"
v.var_name_eff
(Lic.string_of_clock new_base));
let clk = substitute_clock clk in
{ v with var_clock_eff = id,clk }
)
fresh_locs
in
let node_eqs = List.map (substitute (s, new_base)) node_eqs in
let subst_assert x = Lxm.flagit (subst_in_val_exp (s,new_base) x.it) x.src in
let asserts = List.map subst_assert asserts in
let acc = match acc with (a,b,c) -> (a@asserts,b@node_eqs,c@fresh_locs) in
lctx, Some acc
)
| CallByPosLic (_, _)
| Merge (_, _)
| CallByNameLic (_, _) -> lctx, None
and (expand_assert : local_ctx * acc -> val_exp srcflagged -> local_ctx * acc) =
fun (lctx, (a_acc,e_acc,v_acc)) ve ->
(* assert(ve);
is transformed into
assert_var=ve; assert(assert_var);
where assert_var is a fresh new local var
*)
let lxm = ve.src in
let ve = ve.it in
let clk = Lv6Id.of_string "dummy_expand_assert", BaseLic in
let assert_var = new_var "assert" "assert" Bool_type_eff clk in
let assert_eq = Lxm.flagit ([LeftVarLic(assert_var,lxm)], ve) lxm in
let assert_op = Lic.VAR_REF(assert_var.var_name_eff) in
let nve = {
ve_core = CallByPosLic((Lxm.flagit assert_op lxm, []));
ve_typ = [Bool_type_eff];
ve_clk = [BaseLic];
ve_src = lxm
}
in
expand_eq (lctx, ((Lxm.flagit nve lxm)::a_acc, e_acc, assert_var::v_acc)) assert_eq
and (expand_node : local_ctx -> Lic.node_exp -> local_ctx * Lic.node_exp) =
fun lctx n ->
match LicPrg.find_node lctx.curr_prg n.node_key_eff with
| Some n -> lctx, n
| None ->
let lctx, exp_node =
match n.def_eff with
| ExternLic
| AbstractLic _ -> lctx, n
| BodyLic b ->
let locs = get_locals n in
let lctx,acc = List.fold_left expand_eq (lctx, ([],[],locs)) b.eqs_eff in
let lctx,acc = List.fold_left expand_assert (lctx, acc) b.asserts_eff in
let (asserts,neqs, nv) = acc in
let nb = {
eqs_eff = neqs ;
asserts_eff = asserts
}
in
let res =
{ n with
loclist_eff = Some nv;
def_eff = BodyLic nb
}
in
Lv6Verbose.exe ~flag:dbg (fun () ->
Printf.printf "#EN: '%s'\n"
(Lic.string_of_node_key n.node_key_eff));
lctx, res
| MetaOpLic -> lctx, n
in
{ lctx with curr_prg = LicPrg.add_node n.node_key_eff exp_node lctx.curr_prg },
exp_node
(* exported *)
let (doit : Lic.node_key list -> LicPrg.t -> LicPrg.t) =
fun node_calls_to_keep inprg ->
let outprg = LicPrg.empty in
(** types and constants do not change *)
let outprg = LicPrg.fold_types LicPrg.add_type inprg outprg in
let outprg = LicPrg.fold_consts LicPrg.add_const inprg outprg in
let lctx_init = {
init_prg = inprg;
curr_prg = outprg;
keep_node_call = (fun n -> List.mem n node_calls_to_keep);
}
in
(** transform nodes *)
let rec (do_node : Lic.node_key -> Lic.node_exp -> local_ctx -> local_ctx) =
fun nk ne lctx ->
fst (expand_node lctx ne)
in let lctx = LicPrg.fold_nodes do_node inprg lctx_init in
let prg = lctx.curr_prg in
LicPrg.fold_nodes
(fun nk ne acc ->
(* remove expanded nodes *)
if not (List.mem nk node_calls_to_keep) && not (Lic.node_is_extern ne) then
LicPrg.del_node nk acc
else
acc
)
prg
prg