From 39aa0e13c19310bdbaa7bcf3f2f701236206c477 Mon Sep 17 00:00:00 2001 From: Nicolas Berthier Date: Thu, 30 Oct 2014 12:01:25 +0100 Subject: [PATCH] Ugly fix for handling enumerated types when exporting to Controllable-Nbac. To avoid cyclic module dependencies (that show up when trying to compile, e.g, the generated C code), enumerated types declared in the main program are now "moved" into the module containing the generated controllers. --- compiler/heptagon/ctrln/ctrlNbacAsEpt.ml | 12 +-- compiler/main/ctrl2ept.ml | 10 +- compiler/main/mls2seq.ml | 4 +- compiler/minils/ctrln/ctrlNbacGen.ml | 121 ++++++++++++++++++++--- compiler/minils/ctrln/ctrlNbacGen.mli | 2 +- compiler/minils/main/mls_compiler.ml | 6 ++ compiler/utilities/ctrln/ctrln_utils.ml | 7 +- 7 files changed, 135 insertions(+), 27 deletions(-) diff --git a/compiler/heptagon/ctrln/ctrlNbacAsEpt.ml b/compiler/heptagon/ctrln/ctrlNbacAsEpt.ml index 3ea3dc7..c22a649 100644 --- a/compiler/heptagon/ctrln/ctrlNbacAsEpt.ml +++ b/compiler/heptagon/ctrln/ctrlNbacAsEpt.ml @@ -53,11 +53,11 @@ type 'f gen_data = (* --- *) -let mk_gen_data _module_name decls typdefs = +let mk_gen_data qual decls typdefs = { decls; ltyps = label_typs typdefs; - qname = (fun name -> { qual = (* Module module_name *)LocalModule; name }); + qname = (fun name -> { qual; name }); tdefs = SMap.empty; env = Env.empty; var_names = SMap.empty; @@ -300,8 +300,8 @@ let io_of_func gd { fni_io_vars } = (* --- *) -(* /!\ Inputs omitted in the signature w.r.t the Controllable-Nbac model should - not appear anywhere in equations... *) +(* XXX /!\ Inputs omitted in the signature w.r.t the Controllable-Nbac model + should not appear anywhere in equations... *) let io_of_func_match gd { node_inputs; node_outputs } = let decl_arg = function | { a_name = Some n; a_type = ty } -> decl_ident gd (ident_of_name n) ty @@ -346,10 +346,10 @@ let gen_func ?node_sig ~node_name func = (* --- *) -let create_prog modul = +let create_prog ?(open_modul = []) modul = { p_modname = modul; - p_opened = []; + p_opened = open_modul; p_desc = []; } diff --git a/compiler/main/ctrl2ept.ml b/compiler/main/ctrl2ept.ml index b425856..cc4101d 100644 --- a/compiler/main/ctrl2ept.ml +++ b/compiler/main/ctrl2ept.ml @@ -166,6 +166,9 @@ let input_function prog filename node_name node_sig = info "Reading function from `%s'…" filename; let res = parse_n_gen_ept_node ~filename ~node_name ~node_sig () in let node, typs = snd res in + (* XXX: check types are also in signature? maybe we should only use the types + declared in the signature instead, as long as the controller synthesis tool + does not introduce new types. *) let prog = List.fold_right CtrlNbacAsEpt.add_to_prog typs prog in let prog = CtrlNbacAsEpt.add_to_prog node prog in prog @@ -184,6 +187,8 @@ let try_ctrls nn prog = let node_name = Ctrln_utils.controller_node ~num nn in if Modules.check_value node_name then let filename = Ctrln_utils.ctrls_for_node nn num in + if num = 0 && not (Sys.file_exists filename) then + raise Exit; (* abort *) let node_sig = Modules.find_value node_name in let prog = input_function prog filename node_name node_sig in try_ctrls (succ num) prog @@ -203,9 +208,8 @@ let handle_node arg = info "Loading module of controllers for node %s…" (Names.fullname nn); let om = Ctrln_utils.controller_modul mo in Modules.open_module om; - let prog = CtrlNbacAsEpt.create_prog om in - let prog = try_ctrls nn prog in - let prog = if prog.Heptagon.p_desc = [] then try_ctrlf nn prog else prog in + let prog = CtrlNbacAsEpt.create_prog ~open_modul:[ ] om in + let prog = try try_ctrls nn prog with Exit -> try_ctrlf nn prog in output_prog prog om (* -------------------------------------------------------------------------- *) diff --git a/compiler/main/mls2seq.ml b/compiler/main/mls2seq.ml index c7c59e9..3853160 100644 --- a/compiler/main/mls2seq.ml +++ b/compiler/main/mls2seq.ml @@ -109,8 +109,8 @@ let generate_target p s = then List.iter (Mls_printer.print stderr) p_list in*) let { t_program = program; t_name = name } = find_target s in let callgraph p = do_silent_pass "Callgraph" Callgraph.program p in - let mls2obc p = do_silent_pass "Translation into MiniLS" Mls2obc.program p in - let mls2obc_list p_l = do_silent_pass "Translation into MiniLS" (List.map Mls2obc.program) p_l in + let mls2obc p = do_silent_pass "Translation from MiniLS" Mls2obc.program p in + let mls2obc_list p_l = do_silent_pass "Translation from MiniLS" (List.map Mls2obc.program) p_l in match program with | Minils convert_fun -> do_silent_pass "Code generation from MiniLS" convert_fun p diff --git a/compiler/minils/ctrln/ctrlNbacGen.ml b/compiler/minils/ctrln/ctrlNbacGen.ml index 11f6a66..b3fa780 100644 --- a/compiler/minils/ctrln/ctrlNbacGen.ml +++ b/compiler/minils/ctrln/ctrlNbacGen.ml @@ -458,7 +458,7 @@ let var_exp v ty = let decl_arg (v, t) = mk_arg (Some (name v)) t Linearity.Ltop Signature.Cbase -let gen_ctrlf_calls gd node_name equs = +let gen_ctrlf_calls ~requal_types gd node_name equs = let equs, _, _ = List.fold_left begin fun (equs, ubase, num) (u, c) -> @@ -484,6 +484,18 @@ let gen_ctrlf_calls gd node_name equs = let exp = mk_exp ~linearity:Linearity.Ltop Clocks.Cbase (Tprod ot) app in let equ = mk_equation false ov exp in + let is, os = if requal_types then + (* Optional requalification of types declared in the exported module: *) + let requal_arg = function + | { a_type = Tid { qual; name } } as arg when qual = node_name.qual -> + { arg with a_type = Tid { qual = func_name.qual; name } } + | a -> a + in + List.map requal_arg is, List.map requal_arg os + else + is, os + in + (* Declare new node *) let node_sig = Signature.mk_node Location.no_location ~extern:false is os false false [] in @@ -501,7 +513,7 @@ let gen_ctrlf_calls gd node_name equs = (** Node translation. Note the given node is not expored if it does not comprize a contract. *) -let translate_node typdefs : 'n -> 'n * (qualname * 'f AST.node) option = function +let translate_node ~requal_types typdefs = function | ({ n_contract = None } as node) -> node, None | ({ n_name; n_input; n_output; n_local; n_equs; n_contract = Some contr } as node) -> @@ -520,7 +532,7 @@ let translate_node typdefs : 'n -> 'n * (qualname * 'f AST.node) option = functi let gd, contract, locals' = translate_contract ~pref gd contr in let gd, equs' = translate_eqs ~pref (gd, []) n_equs in let gd = assign_uc_groups gd in - let equs' = gen_ctrlf_calls gd n_name equs' in + let equs' = gen_ctrlf_calls ~requal_types gd n_name equs' in let ctrln_node_desc = { cn_typs = typdefs; @@ -541,29 +553,112 @@ let translate_node typdefs : 'n -> 'n * (qualname * 'f AST.node) option = functi (* --- *) +(** Moves all type declarations into the given module, declare aliases for them + (in cases). Also requalifies constructor names in the program, FIXME: as + well as types of expressions to avoid some errors in code generation later + on. *) +let requal_declared_types prog = + + let cmodul = controller_modul prog.p_modname in + let requal m = m = prog.p_modname in + + let requal_it ({ qual; name } as cstr) = + if requal qual then { qual = cmodul; name } else cstr in + + let requal_type = function + | Tid { qual; name } when requal qual -> Tid { qual = cmodul; name } + | t -> t + in + + let open Mls_mapfold in + let open Global_mapfold in + let funcs = { Mls_mapfold.defaults with + + type_dec = (fun _ () -> function + | { t_name = tn; t_desc = Type_enum cl } as t when requal tn.qual -> + let tn' = requal_it tn in + let t = { t with + t_name = tn'; + t_desc = Type_alias (Tid { qual = cmodul; name = tn.name}); + } in + Modules.replace_type tn (Signature.Talias (Tid tn)); + Modules.add_type tn' (Signature.Tenum (List.map requal_it cl)); + t, () + | _ -> raise Errors.Fallback); + + edesc = (fun funs () -> function + | Ewhen (e, c, x) -> + Ewhen (exp_it funs () e |> fst, requal_it c, + var_ident_it funs.global_funs () x |> fst), () + | Emerge (i, l) -> + Emerge (var_ident_it funs.global_funs () i |> fst, + List.map (fun (c, x) -> requal_it c, + extvalue_it funs () x |> fst) l), () + | _ -> raise Errors.Fallback); + + extvalue_desc = (fun funs () -> function + | Wwhen (w, c, v) -> + Wwhen (extvalue_it funs () w |> fst, requal_it c, + var_ident_it funs.global_funs () v |> fst), () + | _ -> raise Errors.Fallback); + + global_funs = { Global_mapfold.defaults with + + ty = (fun _ () ty -> requal_type ty, ()); + + ck = (fun funs () -> function + | Clocks.Con (ck, c, i) -> + Clocks.Con (ck_it funs () ck |> fst, requal_it c, + var_ident_it funs () i |> fst), () + | _ -> raise Errors.Fallback); + + static_exp_desc = (fun _ () -> function + | Sconstructor c -> Sconstructor (requal_it c), () + | _ -> raise Errors.Fallback); + + }; + } in + + program funcs () prog |> fst + +(* --- *) + (** [gen p] translates all type definitions, plus the nodes comprizing a contract, into Controllable-Nbac. @return a Controllable-Nbac program comprizing one process for each node - necessitating controller synthesis), (TODO: and a new Minils program, in - which those nodes have been transformed so that they "call" their respective - controller). *) -let gen ({ p_desc } as p) = + necessitating controller synthesis), and a new Minils program, in which + those nodes have been transformed so that they "call" their respective + controller. + + XXX The [requalify_declared_types] argument is here to avoid cyclic + dependencies between modules due to type declarations. Yet, a better idea + might be to integrate the generated controllers into the original program + later on. *) +let gen ?(requalify_declared_types = true) ({ p_desc } as p) = + + let requal_types = requalify_declared_types in + let _cnp_typs, nodes, descs = - (* XXX Should we gather all the type definitions before translating any - node? *) List.fold_left begin fun (typdefs, nodes, descs) -> function | Pnode n -> - begin match translate_node typdefs n with + begin match translate_node ~requal_types typdefs n with | node, Some n -> (typdefs, n :: nodes, Pnode node :: descs) | node, None -> (typdefs, nodes, Pnode node :: descs) end - | Ptype { t_name = { name }; t_desc = Type_enum cl } -> + | Ptype { t_name = ({ name }); t_desc = Type_enum cl } as ty -> let tn = mk_typname & mk_symb name and typ = translate_constrs cl in let typdefs = declare_typ tn typ typdefs in - (typdefs, nodes, descs) + (typdefs, nodes, ty :: descs) | p -> (typdefs, nodes, p :: descs) end (empty_typdefs, [], []) p_desc in + let cnp_nodes = List.rev nodes and p_desc = List.rev descs in - cnp_nodes, { p with p_desc } + let prog = { p with p_desc } in + let prog = (* moving types to controller module? *) + if requalify_declared_types + then requal_declared_types prog + else prog + in + cnp_nodes, prog diff --git a/compiler/minils/ctrln/ctrlNbacGen.mli b/compiler/minils/ctrln/ctrlNbacGen.mli index 6355d65..28415fd 100644 --- a/compiler/minils/ctrln/ctrlNbacGen.mli +++ b/compiler/minils/ctrln/ctrlNbacGen.mli @@ -31,5 +31,5 @@ (* Interface documentation is in `ctrlNbacGen.ml' only. *) (** *) -val gen: Minils.program -> +val gen: ?requalify_declared_types:bool -> Minils.program -> (Names.qualname * 'f CtrlNbac.AST.node) list * Minils.program diff --git a/compiler/minils/main/mls_compiler.ml b/compiler/minils/main/mls_compiler.ml index f128167..ab92000 100644 --- a/compiler/minils/main/mls_compiler.ml +++ b/compiler/minils/main/mls_compiler.ml @@ -41,8 +41,14 @@ let pp p = if !verbose then Mls_printer.print stdout p under a specific directory; typically, a node ["n"] in file ["f.ept"] is output into a file called "f_ctrln/n.nbac" *) let gen_n_output_ctrln p = + + (* Main generation procedure. *) let nodes, p = CtrlNbacGen.gen p in + + (* Save the controller module. *) Ctrln_utils.save_controller_modul_for p.Minils.p_modname; + + (* Output Controllable-Nbac contoller. *) ignore (clean_dir (Ctrln_utils.dirname_for_modul p.Minils.p_modname)); List.iter begin fun (node_name, node) -> let oc = open_out (Ctrln_utils.ctrln_for_node node_name) in diff --git a/compiler/utilities/ctrln/ctrln_utils.ml b/compiler/utilities/ctrln/ctrln_utils.ml index 59dc4e9..b8912d1 100644 --- a/compiler/utilities/ctrln/ctrln_utils.ml +++ b/compiler/utilities/ctrln/ctrln_utils.ml @@ -30,6 +30,8 @@ open Compiler_utils open Names +let ctrlr_mod_suffix = "_controller" + let dirname_for_modul modul = build_path (filename_of_name (modul_to_string modul) ^ "_ctrln") @@ -43,8 +45,9 @@ let ctrlf_for_node { qual; name } = Printf.sprintf "%s/%s.ctrlf" (dirname_for_modul qual) name let controller_modul = function - | Module n -> Module (n ^ "_ctrls") - | QualModule ({ name = n } as q) -> QualModule { q with name = n ^ "_ctrls" } + | Module n -> Module (n ^ ctrlr_mod_suffix) + | QualModule ({ name = n } as q) -> + QualModule { q with name = n ^ ctrlr_mod_suffix } | _ -> failwith "Unexpected module" let controller_node ?num { qual; name } = match num with