From 2f993a602c6de6ed504f3aecc3cd04e9b8070249 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?C=C3=A9dric=20Pasteur?= Date: Wed, 25 Jan 2012 09:34:58 +0100 Subject: [PATCH] Fixed base clock in code generation Put the base clock inside the equation where it belongs. --- compiler/global/clocks.ml | 6 +++- compiler/main/mls2obc.ml | 5 ++-- compiler/minils/analysis/clocking.ml | 29 ++++++++++--------- compiler/minils/analysis/interference.ml | 6 +++- compiler/minils/analysis/level_clock.ml | 7 ++--- compiler/minils/minils.ml | 12 ++++---- compiler/minils/mls_compare.ml | 3 -- compiler/minils/mls_mapfold.ml | 6 ++-- compiler/minils/mls_printer.ml | 4 +-- compiler/minils/mls_utils.ml | 2 +- compiler/minils/sigali/sigalimain.ml | 4 +-- .../transformations/inline_extvalues.ml | 8 +++-- .../minils/transformations/schedule_interf.ml | 10 +++---- compiler/minils/transformations/tomato.ml | 9 +++--- 14 files changed, 60 insertions(+), 51 deletions(-) diff --git a/compiler/global/clocks.ml b/compiler/global/clocks.ml index 58e237f..dd8216a 100644 --- a/compiler/global/clocks.ml +++ b/compiler/global/clocks.ml @@ -138,4 +138,8 @@ let same_control ck1 ck2 = match ck_repr ck1, ck_repr ck2 with | Cvar {contents = Cindex i1}, Cvar {contents = Cindex i2} -> i1 = i2 | _ -> false - +(** returns the first clock of a ct. *) +let rec first_ck ct = match ct with + | Ck ck -> ck + | Cprod [] -> assert false + | Cprod (ct::_) -> first_ck ct diff --git a/compiler/main/mls2obc.ml b/compiler/main/mls2obc.ml index dd45174..bc81412 100644 --- a/compiler/main/mls2obc.ml +++ b/compiler/main/mls2obc.ml @@ -434,9 +434,10 @@ let empty_call_context = None [j] obj decs [s] the actions used in the step method. [v] var decs *) -let rec translate_eq map call_context ({ Minils.eq_lhs = pat; Minils.eq_rhs = e } as eq) +let rec translate_eq map call_context + ({ Minils.eq_lhs = pat; Minils.eq_base_ck = ck; Minils.eq_rhs = e } as eq) (v, si, j, s) = - let { Minils.e_desc = desc; Minils.e_base_ck = ck; Minils.e_loc = loc } = e in + let { Minils.e_desc = desc; Minils.e_loc = loc } = e in match (pat, desc) with | pat, Minils.Ewhen (e,_,_) -> translate_eq map call_context {eq with Minils.eq_rhs = e} (v, si, j, s) diff --git a/compiler/minils/analysis/clocking.ml b/compiler/minils/analysis/clocking.ml index 73a9f57..13f4877 100644 --- a/compiler/minils/analysis/clocking.ml +++ b/compiler/minils/analysis/clocking.ml @@ -144,7 +144,7 @@ let rec stateful e = match e.e_desc with | _ -> false -let typing_eq h { eq_lhs = pat; eq_rhs = e; eq_loc = loc } = +let typing_eq h ({ eq_lhs = pat; eq_rhs = e; eq_loc = loc } as eq) = (* typing the expression, returns ct, ck_base *) let rec typing e = let ct,base = match e.e_desc with @@ -201,7 +201,6 @@ let typing_eq h { eq_lhs = pat; eq_rhs = e; eq_loc = loc } = in ct, base_ck in - e.e_base_ck <- base; (try unify ct e.e_ct with Unify -> eprintf "Inconsistent clock annotation for exp %a.@\n" @@ -215,14 +214,15 @@ let typing_eq h { eq_lhs = pat; eq_rhs = e; eq_loc = loc } = with Unify -> error_message e.e_loc (Etypeclash (actual_ct, expected_ct))); base in - let ct,_ = typing e in + let ct,base_ck = typing e in let pat_ct = typing_pat h pat in (try unify ct pat_ct with Unify -> eprintf "Incoherent clock between right and left side of the equation.@\n"; - error_message loc (Etypeclash (ct, pat_ct))) + error_message loc (Etypeclash (ct, pat_ct))); + { eq with eq_base_ck = base_ck } -let typing_eqs h eq_list = List.iter (typing_eq h) eq_list +let typing_eqs h eq_list = List.map (typing_eq h) eq_list let append_env h vds = List.fold_left (fun h { v_ident = n; v_clock = ck } -> Env.add n ck h) h vds @@ -230,34 +230,37 @@ let append_env h vds = let typing_contract h contract = match contract with - | None -> h - | Some { c_local = l_list; + | None -> None, h + | Some ({ c_local = l_list; c_eq = eq_list; c_assume = e_a; c_enforce = e_g; - c_controllables = c_list } -> + c_controllables = c_list } as contract) -> let h' = append_env h l_list in (* assumption *) (* property *) - typing_eqs h' eq_list; + let eq_list = typing_eqs h' eq_list in expect_extvalue h' Cbase e_a; expect_extvalue h' Cbase e_g; - append_env h c_list + let h = append_env h c_list in + Some { contract with c_eq = eq_list }, h let typing_node node = let h0 = append_env Env.empty node.n_input in let h0 = append_env h0 node.n_output in - let h = typing_contract h0 node.n_contract in + let contract, h = typing_contract h0 node.n_contract in let h = append_env h node.n_local in - typing_eqs h node.n_equs; + let equs = typing_eqs h node.n_equs in (* synchronize input and output on base : find the free vars and set them to base *) Env.iter (fun _ ck -> unify_ck Cbase (root_ck_of ck)) h0; (*update clock info in variables descriptions *) let set_clock vd = { vd with v_clock = ck_repr (Env.find vd.v_ident h) } in let node = { node with n_input = List.map set_clock node.n_input; n_output = List.map set_clock node.n_output; - n_local = List.map set_clock node.n_local } + n_local = List.map set_clock node.n_local; + n_equs = equs; + n_contract = contract; } in let sign = Mls_utils.signature_of_node node in Check_signature.check_signature sign; diff --git a/compiler/minils/analysis/interference.ml b/compiler/minils/analysis/interference.ml index d3f0ab6..026b511 100644 --- a/compiler/minils/analysis/interference.ml +++ b/compiler/minils/analysis/interference.ml @@ -60,6 +60,10 @@ module InterfRead = struct | Cbase | Cvar { contents = Cindex _ } -> acc | Cvar { contents = Clink ck } -> vars_ck acc ck + let rec vars_ct acc ct = match ct with + | Ck ck -> vars_ck acc ck + | Cprod ct_list -> List.fold_left vars_ct acc ct_list + let rec ivar_of_extvalue w = match w.w_desc with | Wvar x -> Ivar x | Wfield(w, f) -> Ifield (ivar_of_extvalue w, f) @@ -100,7 +104,7 @@ module InterfRead = struct | Eiterator (_, _, _, _, _, Some x) -> IvarSet.add (Ivar x) acc | _ -> acc in - e, vars_ck acc e.e_base_ck + e, vars_ct acc e.e_ct let rec vars_pat acc = function | Evarpat x -> IvarSet.add (Ivar x) acc diff --git a/compiler/minils/analysis/level_clock.ml b/compiler/minils/analysis/level_clock.ml index 605efca..2da36ba 100644 --- a/compiler/minils/analysis/level_clock.ml +++ b/compiler/minils/analysis/level_clock.ml @@ -20,9 +20,8 @@ open Minils indeed if it was Con (Cvar,c,x) x would have to be defined with an expression of clock Cvar.*) let eq _ acc eq = - let e = eq.eq_rhs in - let _ = match ck_repr e.e_base_ck with - | Cvar {contents = Cindex _} -> unify_ck e.e_base_ck e.e_level_ck + let _ = match ck_repr eq.eq_base_ck with + | Cvar {contents = Cindex _} -> unify_ck eq.eq_base_ck eq.eq_rhs.e_level_ck | _ -> () in eq,acc (* no recursion since in minils exps are not recursive *) @@ -30,4 +29,4 @@ let eq _ acc eq = let program p = let funs = { Mls_mapfold.defaults with Mls_mapfold.eq = eq } in let p, _ = Mls_mapfold.program_it funs [] p in - p \ No newline at end of file + p diff --git a/compiler/minils/minils.ml b/compiler/minils/minils.ml index e58e111..3b405bb 100644 --- a/compiler/minils/minils.ml +++ b/compiler/minils/minils.ml @@ -57,7 +57,6 @@ and extvalue_desc = and exp = { e_desc : edesc; e_level_ck : ck; (*when no data dep, execute the exp on this clock (set by [switch] *) - mutable e_base_ck : ck; mutable e_ct : ct; e_ty : ty; e_linearity : linearity; @@ -109,6 +108,7 @@ type eq = { eq_lhs : pat; eq_rhs : exp; eq_unsafe : bool; + eq_base_ck : ck; eq_loc : location } type var_dec = { @@ -196,21 +196,21 @@ let mk_vd_extvalue vd = mk_extvalue ~ty:vd.v_type ~linearity:vd.v_linearity ~clock:vd.v_clock ~loc:vd.v_loc (Wvar vd.v_ident) -let mk_exp level_ck ty ~linearity ?(ck = Cbase) +let mk_exp level_ck ty ~linearity ?(ct = fresh_ct ty) ?(loc = no_location) desc = { e_desc = desc; e_ty = ty; e_linearity = linearity; - e_level_ck = level_ck; e_base_ck = ck; e_ct = ct; e_loc = loc } + e_level_ck = level_ck; e_ct = ct; e_loc = loc } let mk_var_dec ?(loc = no_location) ident ty linearity ck = { v_ident = ident; v_type = ty; v_linearity = linearity; v_clock = ck; v_loc = loc } let mk_extvalue_exp ?(clock = fresh_clock()) ?(loc = no_location) level_ck ty ~linearity desc = - mk_exp ~ck:clock ~loc:loc level_ck ty ~linearity:linearity + mk_exp ~loc:loc level_ck ty ~linearity:linearity (Eextvalue (mk_extvalue ~clock:clock ~loc:loc ~linearity:linearity ~ty:ty desc)) -let mk_equation ?(loc = no_location) unsafe pat exp = - { eq_lhs = pat; eq_rhs = exp; eq_unsafe = unsafe; eq_loc = loc } +let mk_equation ?(loc = no_location) ?(base_ck=fresh_clock()) unsafe pat exp = + { eq_lhs = pat; eq_rhs = exp; eq_unsafe = unsafe; eq_base_ck = base_ck; eq_loc = loc } let mk_node ?(input = []) ?(output = []) ?(contract = None) ?(pinst = ([],[])) diff --git a/compiler/minils/mls_compare.ml b/compiler/minils/mls_compare.ml index 05330f1..00c43b8 100644 --- a/compiler/minils/mls_compare.ml +++ b/compiler/minils/mls_compare.ml @@ -61,9 +61,6 @@ struct else let cr = Linearity.linearity_compare e1.e_linearity e2.e_linearity in if cr <> 0 then cr - else - let cr = C.clock_compare e1.e_base_ck e2.e_base_ck in - if cr <> 0 then cr else match e1.e_desc, e2.e_desc with | Eextvalue w1, Eextvalue w2 -> diff --git a/compiler/minils/mls_mapfold.ml b/compiler/minils/mls_mapfold.ml index 2d30950..da6c5a5 100644 --- a/compiler/minils/mls_mapfold.ml +++ b/compiler/minils/mls_mapfold.ml @@ -41,11 +41,10 @@ let rec exp_it funs acc e = funs.exp funs acc e and exp funs acc e = let e_ty, acc = ty_it funs.global_funs acc e.e_ty in let e_level_ck, acc = ck_it funs.global_funs acc e.e_level_ck in - let e_base_ck, acc = ck_it funs.global_funs acc e.e_base_ck in let e_ct, acc = ct_it funs.global_funs acc e.e_ct in let ed, acc = edesc_it funs acc e.e_desc in { e with e_desc = ed; e_ty = e_ty; e_level_ck = e_level_ck; - e_base_ck = e_base_ck; e_ct = e_ct }, acc + e_ct = e_ct }, acc and extvalue_it funs acc w = funs.extvalue funs acc w and extvalue funs acc w = @@ -141,8 +140,9 @@ and pat funs acc p = match p with and eq_it funs acc eq = funs.eq funs acc eq and eq funs acc eq = let eq_lhs, acc = pat_it funs acc eq.eq_lhs in + let eq_base_ck, acc = ck_it funs.global_funs acc eq.eq_base_ck in let eq_rhs, acc = exp_it funs acc eq.eq_rhs in - { eq with eq_lhs = eq_lhs; eq_rhs = eq_rhs }, acc + { eq with eq_lhs = eq_lhs; eq_rhs = eq_rhs; eq_base_ck = eq_base_ck }, acc and eqs_it funs acc eqs = funs.eqs funs acc eqs and eqs funs acc eqs = mapfold (eq_it funs) acc eqs diff --git a/compiler/minils/mls_printer.ml b/compiler/minils/mls_printer.ml index cea19a2..822364b 100644 --- a/compiler/minils/mls_printer.ml +++ b/compiler/minils/mls_printer.ml @@ -173,10 +173,10 @@ and print_tag_w_list ff tag_w_list = fprintf ff "@[%a@]" (print_list print_handler """""") tag_w_list -and print_eq ff { eq_lhs = p; eq_rhs = e } = +and print_eq ff { eq_lhs = p; eq_rhs = e; eq_base_ck = base_ck } = if !Compiler_options.full_type_info then fprintf ff "@[<2>%a :: %a =@ %a@]" - print_pat p print_ck e.e_base_ck print_exp e + print_pat p print_ck base_ck print_exp e else fprintf ff "@[<2>%a =@ %a@]" print_pat p print_exp e diff --git a/compiler/minils/mls_utils.ml b/compiler/minils/mls_utils.ml index 6c5c4eb..94cd70e 100644 --- a/compiler/minils/mls_utils.ml +++ b/compiler/minils/mls_utils.ml @@ -156,7 +156,7 @@ struct let antidep { eq_rhs = e } = is_fby e - let clock { eq_rhs = e } = e.e_base_ck + let clock eq = eq.eq_base_ck let head ck = let rec headrec ck l = diff --git a/compiler/minils/sigali/sigalimain.ml b/compiler/minils/sigali/sigalimain.ml index f3e8b20..abecb59 100644 --- a/compiler/minils/sigali/sigalimain.ml +++ b/compiler/minils/sigali/sigalimain.ml @@ -184,13 +184,13 @@ let rec translate prefix ({ Minils.e_desc = desc; Minils.e_ty = ty } as e) = let rec translate_eq env f (acc_dep,acc_states,acc_init,acc_inputs,acc_ctrl,acc_cont,acc_eqs) - { Minils.eq_lhs = pat; Minils.eq_rhs = e } = + { Minils.eq_lhs = pat; Minils.eq_rhs = e; eq_base_ck = ck } = let prefix = f ^ "_" in let prefixed n = prefix ^ n in - let { Minils.e_desc = desc; Minils.e_base_ck = ck } = e in + let { Minils.e_desc = desc } = e in match pat, desc with | Minils.Evarpat(n), Minils.Efby(opt_c, e) -> let sn = prefixed (name n) in diff --git a/compiler/minils/transformations/inline_extvalues.ml b/compiler/minils/transformations/inline_extvalues.ml index 71bf64a..b6d9482 100644 --- a/compiler/minils/transformations/inline_extvalues.ml +++ b/compiler/minils/transformations/inline_extvalues.ml @@ -98,14 +98,16 @@ let form_new_extvalue_node nd = let rec form_new_extvalue e = try let se = form_new_const e in - mk_extvalue ~ty:e.e_ty ~linearity:e.e_linearity ~clock:e.e_base_ck ~loc:e.e_loc (Wconst se) + mk_extvalue ~ty:e.e_ty ~linearity:e.e_linearity + ~clock:(Clocks.first_ck e.e_ct) ~loc:e.e_loc (Wconst se) with Errors.Fallback -> let w_d = match e.e_desc with | Eextvalue w -> w.w_desc | Ewhen (e, v, x) -> Wwhen (form_new_extvalue e, v, x) | _ -> raise Errors.Fallback in - mk_extvalue ~ty:e.e_ty ~linearity:e.e_linearity ~clock:e.e_base_ck ~loc:e.e_loc w_d + mk_extvalue ~ty:e.e_ty ~linearity:e.e_linearity + ~clock:(Clocks.first_ck e.e_ct) ~loc:e.e_loc w_d and form_new_const e = let se_d = match e.e_desc with @@ -135,7 +137,7 @@ let form_new_extvalue_node nd = and form_new_const_w w = let mk_exp w = - mk_exp w.w_ck w.w_ty ~linearity:w.w_linearity ~ck:w.w_ck ~ct:(Ck w.w_ck) (Eextvalue w) in + mk_exp w.w_ck w.w_ty ~linearity:w.w_linearity ~ct:(Ck w.w_ck) (Eextvalue w) in form_new_const (mk_exp w) and form_new_extvalue_eq _ n eq = match eq.eq_rhs.e_desc with diff --git a/compiler/minils/transformations/schedule_interf.ml b/compiler/minils/transformations/schedule_interf.ml index ea7c3be..2f20da8 100644 --- a/compiler/minils/transformations/schedule_interf.ml +++ b/compiler/minils/transformations/schedule_interf.ml @@ -7,9 +7,6 @@ open Misc open Sgraph -let eq_clock eq = - eq.eq_rhs.e_base_ck - module Cost = struct open Interference_graph @@ -76,7 +73,10 @@ struct min_same_ck (min_eq, min_c, min_same_ctrl) l in let eqs_wcost = - List.map (fun eq -> (eq, cost eq, Clocks.same_control (eq_clock eq) ck)) rem_eqs in + List.map + (fun eq -> (eq, cost eq, Clocks.same_control (Mls_utils.Vars.clock eq) ck)) + rem_eqs + in let (eq, c, same_ctrl), eqs_wcost = Misc.assert_1min eqs_wcost in min_same_ck (eq, c, same_ctrl) eqs_wcost end @@ -125,7 +125,7 @@ let schedule eq_list inputs node_list = let rem_eqs = free_eqs node_list in (* compute new costs for the next step *) let costs = Cost.update_cost eq uses costs in - schedule_aux rem_eqs (eq::sched_eqs) node_list (eq_clock eq) costs + schedule_aux rem_eqs (eq::sched_eqs) node_list (Mls_utils.Vars.clock eq) costs in let costs = Cost.init_cost uses inputs in let rem_eqs = free_eqs node_list in diff --git a/compiler/minils/transformations/tomato.ml b/compiler/minils/transformations/tomato.ml index bda455e..ed9c57b 100644 --- a/compiler/minils/transformations/tomato.ml +++ b/compiler/minils/transformations/tomato.ml @@ -211,7 +211,7 @@ let rec add_equation is_input (tenv : tom_env) eq = let ed, add_when, when_count, class_id_list = decompose e' in ed, (fun e' -> { e with e_desc = Ewhen (add_when e', cn, x) }), when_count + 1, class_ref_of_var is_input - (mk_extvalue ~clock:e'.e_base_ck ~ty:Initial.tbool + (mk_extvalue ~clock:(Clocks.first_ck e'.e_ct) ~ty:Initial.tbool ~linearity:Linearity.Ltop (Wvar x)) x :: class_id_list @@ -219,7 +219,7 @@ let rec add_equation is_input (tenv : tom_env) eq = let class_id_list, clause_list = mapfold_right add_clause clause_list [] in let x_id = class_ref_of_var is_input - (mk_extvalue ~clock:e.e_base_ck ~ty:Initial.tbool + (mk_extvalue ~clock:(Clocks.first_ck e.e_ct) ~ty:Initial.tbool ~linearity:Linearity.Ltop (Wvar x)) x in Emerge (dummy_var, clause_list), id, 0, x_id :: class_id_list @@ -363,12 +363,11 @@ let rec reconstruct ((tenv, cenv) as env) mapping = Misc.take (List.length repr.er_children - repr.er_when_count) repr.er_children in let ed = reconstruct_exp_desc mapping repr.er_head.e_desc repr.er_children in - let ck = reconstruct_clock mapping repr.er_head.e_base_ck in let level_ck = reconstruct_clock mapping repr.er_head.e_level_ck in (* not strictly needed, done for consistency reasons *) let ct = reconstruct_clock_type mapping repr.er_head.e_ct in - { repr.er_head with e_desc = ed; e_base_ck = ck; e_level_ck = level_ck; e_ct = ct; } in + { repr.er_head with e_desc = ed; e_level_ck = level_ck; e_ct = ct; } in let e = repr.er_add_when e in @@ -577,7 +576,7 @@ let rec fix_output_var_dec mapping vd (seen, equs, vd_list) = mk_equation false (Evarpat new_id) (mk_exp new_clock vd.v_type ~ct:(Ck new_clock) - ~ck:new_clock ~linearity:Linearity.Ltop (Eextvalue w)) + ~linearity:Linearity.Ltop (Eextvalue w)) in (seen, new_eq :: equs, new_vd :: vd_list) else