diff --git a/compiler/global/modules.ml b/compiler/global/modules.ml index 3c45afc..54b902d 100644 --- a/compiler/global/modules.ml +++ b/compiler/global/modules.ml @@ -140,6 +140,14 @@ let add_const f n = if NamesEnv.mem f current.consts then raise Already_defined; current.consts <- NamesEnv.add f n current.consts +let add_value_by_longname ln signature = + match ln with + | Modname { qual = modname; id = f } -> + let m = NamesEnv.find modname modules.modules in + if NamesEnv.mem f m.values then raise Already_defined; + m.values <- NamesEnv.add f signature m.values + | Name _ -> raise Not_found + let find_value = find (fun ident m -> NamesEnv.find ident m.values) let find_type = find (fun ident m -> NamesEnv.find ident m.types) let find_constr = find (fun ident m -> NamesEnv.find ident m.constr) diff --git a/compiler/global/names.ml b/compiler/global/names.ml index 75ca7e0..96c7f79 100644 --- a/compiler/global/names.ml +++ b/compiler/global/names.ml @@ -34,6 +34,11 @@ struct fold (fun key v env -> add key v env) env0 env end +module LongNameEnv = Map.Make (struct + type t = longname + let compare = compare + end) + module S = Set.Make (struct type t = string let compare = compare end) diff --git a/compiler/global/static.ml b/compiler/global/static.ml index 129006a..5bfd18a 100644 --- a/compiler/global/static.ml +++ b/compiler/global/static.ml @@ -132,7 +132,7 @@ let rec static_exp_subst m se = match se.se_desc with | Svar ln -> (match ln with - | Name n -> (try List.assoc n m with | Not_found -> se) + | Name n -> (try NamesEnv.find n m with | Not_found -> se) | Modname _ -> se) | Sop (op, se_list) -> { se with se_desc = Sop (op, List.map (static_exp_subst m) se_list) } diff --git a/compiler/global/types.ml b/compiler/global/types.ml index d24f4db..feb213a 100644 --- a/compiler/global/types.ml +++ b/compiler/global/types.ml @@ -32,6 +32,8 @@ let invalid_type = Tprod [] let mk_static_exp ?(loc = no_location) ?(ty = invalid_type) desc = { se_desc = desc; se_ty = ty; se_loc = loc } +let static_exp_of_int i = + mk_static_exp (Sint i) open Pp_tools open Format diff --git a/compiler/heptagon/analysis/typing.ml b/compiler/heptagon/analysis/typing.ml index 5ff9980..1b075b6 100644 --- a/compiler/heptagon/analysis/typing.ml +++ b/compiler/heptagon/analysis/typing.ml @@ -340,6 +340,10 @@ let simplify_type loc ty = with Instanciation_failed -> message loc (Etype_should_be_static ty) +let build_subst names values = + List.fold_left2 (fun m { p_name = n } v -> NamesEnv.add n v m) + NamesEnv.empty names values + let rec subst_type_vars m = function | Tarray(ty, e) -> Tarray(subst_type_vars m ty, static_exp_subst m e) | Tprod l -> Tprod (List.map (subst_type_vars m) l) @@ -621,8 +625,7 @@ let rec typing statefull const_env h e = let { qualid = q; info = ty_desc } = find_value f in let op, expected_ty_list, result_ty_list = kind f statefull ty_desc in - let m = List.combine - (List.map (fun p -> p.p_name) ty_desc.node_params) params in + let m = build_subst ty_desc.node_params params in let expected_ty_list = List.map (subst_type_vars m) expected_ty_list in let result_ty_list = List.map (subst_type_vars m) result_ty_list in @@ -678,8 +681,7 @@ and typing_app statefull const_env h op e_list = let { qualid = q; info = ty_desc } = find_value f in let op, expected_ty_list, result_ty_list = kind (Modname q) statefull ty_desc in - let m = List.combine (List.map (fun p -> p.p_name) ty_desc.node_params) - params in + let m = build_subst ty_desc.node_params params in let expected_ty_list = List.map (subst_type_vars m) expected_ty_list in let typed_e_list = typing_args statefull const_env h expected_ty_list e_list in diff --git a/compiler/heptagon/heptagon.ml b/compiler/heptagon/heptagon.ml index 5da15cf..85ec5c1 100644 --- a/compiler/heptagon/heptagon.ml +++ b/compiler/heptagon/heptagon.ml @@ -123,6 +123,7 @@ type const_dec = { c_loc : location } type program = { + p_modname : name; p_opened : name list; p_types : type_dec list; p_nodes : node_dec list; diff --git a/compiler/heptagon/parsing/hept_parser.mly b/compiler/heptagon/parsing/hept_parser.mly index 9d30eda..27f9bb3 100644 --- a/compiler/heptagon/parsing/hept_parser.mly +++ b/compiler/heptagon/parsing/hept_parser.mly @@ -87,11 +87,12 @@ let mk_static_exp = mk_static_exp ~loc:(current_loc()) program: | pragma_headers open_modules const_decs type_decs node_decs EOF - {{ p_pragmas = $1; - p_opened = List.rev $2; + {{ p_modname = ""; + p_pragmas = $1; + p_opened = List.rev $2; p_types = $4; p_nodes = $5; - p_consts = $3; }} + p_consts = $3; }} ; pragma_headers: diff --git a/compiler/heptagon/parsing/hept_parsetree.ml b/compiler/heptagon/parsing/hept_parsetree.ml index f3643bf..ec6b452 100644 --- a/compiler/heptagon/parsing/hept_parsetree.ml +++ b/compiler/heptagon/parsing/hept_parsetree.ml @@ -138,7 +138,8 @@ type const_dec = c_loc : location; } type program = - { p_pragmas: (name * string) list; + { p_modname : name; + p_pragmas: (name * string) list; p_opened : name list; p_types : type_dec list; p_nodes : node_dec list; diff --git a/compiler/heptagon/parsing/hept_scoping.ml b/compiler/heptagon/parsing/hept_scoping.ml index 4345bf5..7508ab9 100644 --- a/compiler/heptagon/parsing/hept_scoping.ml +++ b/compiler/heptagon/parsing/hept_scoping.ml @@ -317,7 +317,8 @@ let translate_const_dec const_env cd = let translate_program p = let const_env = build_cd_list NamesEnv.empty p.p_consts in - { Heptagon.p_opened = p.p_opened; + { Heptagon.p_modname = p.p_modname; + Heptagon.p_opened = p.p_opened; Heptagon.p_types = List.map (translate_typedec const_env) p.p_types; Heptagon.p_nodes = List.map (translate_node const_env Rename.empty) p.p_nodes; diff --git a/compiler/main/hept2mls.ml b/compiler/main/hept2mls.ml index 96c14d5..5aeb80f 100644 --- a/compiler/main/hept2mls.ml +++ b/compiler/main/hept2mls.ml @@ -205,26 +205,27 @@ let rec translate_op env = function | Heptagon.Econcat -> Econcat | Heptagon.Earray -> Earray | Heptagon.Etuple -> Etuple - | Heptagon.Earrow -> Earrow + | Heptagon.Earrow -> + Error.message no_location Error.Eunsupported_language_construct let translate_app env app = - mk_app ~params:app.a_params - ~unsafe:app.a_unsafe (translate_op env app.a_op) + mk_app ~params:app.Heptagon.a_params + ~unsafe:app.Heptagon.a_unsafe (translate_op env app.Heptagon.a_op) let rec translate env { Heptagon.e_desc = desc; Heptagon.e_ty = ty; Heptagon.e_loc = loc } = match desc with | Heptagon.Econst c -> - Env.const env (mk_exp ~loc:loc ~exp_ty:ty (Econst (const c))) + Env.const env (mk_exp ~loc:loc ~exp_ty:ty (Econst c)) | Heptagon.Evar x -> Env.con env x (mk_exp ~loc:loc ~exp_ty:ty (Evar x)) - | Heptagon.Epre(None), [e] -> - mk_exp ~loc:loc ~exp_ty:ty (Efby(None, e)) + | Heptagon.Epre(None, e) -> + mk_exp ~loc:loc ~exp_ty:ty (Efby(None, translate env e)) | Heptagon.Epre(Some c, e) -> - mk_exp ~loc:loc ~exp_ty:ty (Efby(Some c, e)) - | Heptagon.Efby ({ e_desc = Econst c }, e) -> - mk_exp ~loc:loc ~exp_ty:ty (Efby(Some c, e)) + mk_exp ~loc:loc ~exp_ty:ty (Efby(Some c, translate env e)) + | Heptagon.Efby ({ Heptagon.e_desc = Heptagon.Econst c }, e) -> + mk_exp ~loc:loc ~exp_ty:ty (Efby(Some c, translate env e)) | Heptagon.Efield(e, field) -> assert false (**TODO *) | Heptagon.Estruct f_e_list -> @@ -232,14 +233,15 @@ let rec translate env (fun (f, e) -> (f, translate env e)) f_e_list in mk_exp ~loc:loc ~exp_ty:ty (Estruct f_e_list) | Heptagon.Eapp(app, e_list, reset) -> - mk_exp ~loc:loc ~exp_ty:ty (translate_app env app, - List.map (translate env) e_list, - translate_reset env reset) + mk_exp ~loc:loc ~exp_ty:ty (Eapp (translate_app env app, + List.map (translate env) e_list, + translate_reset reset)) | Heptagon.Eiterator(it, app, n, e_list, reset) -> - mk_exp ~loc:loc ~exp_ty:ty Eiterator(translate_iterator_type it, - translate_app env app, n, - List.map (translate env) e_list, - translate_reset reset) + mk_exp ~loc:loc ~exp_ty:ty + (Eiterator (translate_iterator_type it, + translate_app env app, n, + List.map (translate env) e_list, + translate_reset reset)) | Heptagon.Elast _ -> Error.message loc Error.Eunsupported_language_construct @@ -341,7 +343,6 @@ let translate_contract env contract = Heptagon.c_eq = eq_list; Heptagon.c_assume = e_a; Heptagon.c_enforce = e_g} -> - let env = Env.add cl env in let env' = Env.add v env in let locals = translate_locals [] v in let locals, l_eqs, s_eqs = @@ -392,17 +393,19 @@ let typedec { t_name = n; t_desc = onetype tdesc; t_loc = loc } let const_dec cd = - { c_name = cd.Heptagon.c_name; - c_value = cd.Heptagon.c_value; - c_loc = cd.Heptagon.c_loc; } + { Minils.c_name = cd.Heptagon.c_name; + Minils.c_value = cd.Heptagon.c_value; + Minils.c_type = cd.Heptagon.c_type; + Minils.c_loc = cd.Heptagon.c_loc; } let program - { Heptagon.p_pragmas = pragmas; + { Heptagon.p_modname = modname; Heptagon.p_opened = modules; Heptagon.p_types = pt_list; Heptagon.p_nodes = n_list; Heptagon.p_consts = c_list; } = - { p_pragmas = pragmas; + { p_modname = modname; + p_format_version = minils_format_version; p_opened = modules; p_types = List.map typedec pt_list; p_nodes = List.map node n_list; diff --git a/compiler/main/heptc.ml b/compiler/main/heptc.ml index a4a5419..1e77e23 100644 --- a/compiler/main/heptc.ml +++ b/compiler/main/heptc.ml @@ -19,22 +19,16 @@ let compile_impl modname filename = (* input and output files *) let source_name = filename ^ ".ept" and obj_interf_name = filename ^ ".epci" - and mls_name = filename ^ ".mls" - and obc_name = filename ^ ".obc" - and ml_name = filename ^ ".ml" in + and mls_name = filename ^ ".mls" in let ic = open_in source_name and itc = open_out_bin obj_interf_name - and mlsc = open_out mls_name - and obc = open_out obc_name - and mlc = open_out ml_name in + and mlsc = open_out mls_name in let close_all_files () = close_in ic; close_out itc; - close_out mlsc; - close_out obc; - close_out mlc in + close_out mlsc in try init_compiler modname source_name ic; @@ -42,6 +36,7 @@ let compile_impl modname filename = (* Parsing of the file *) let lexbuf = Lexing.from_channel ic in let p = parse_implementation lexbuf in + let p = { p with Hept_parsetree.p_modname = modname } in (* Convert the parse tree to Heptagon AST *) let p = Hept_scoping.translate_program p in @@ -61,18 +56,10 @@ let compile_impl modname filename = Mls_printer.print mlsc p; (* Process the MiniLS AST *) - let p = Mls_compiler.compile pp p in + (* let p = Mls_compiler.compile pp p in *) - (* Compile MiniLS to Obc *) - let o = Mls2obc.program p in - comment "Translation into Obc"; - Obc_printer.print obc o; - - let pp = Obc_printer.print stdout in - if !verbose then pp o; - - (* Translation into dataflow and sequential languages *) - Mls2seq.targets filename p o !target_languages; + (* Generate the sequential code *) + Mls2seq.program p; close_all_files () @@ -91,6 +78,7 @@ let main () = "-I", Arg.String add_include, doc_include; "-where", Arg.Unit locate_stdlib, doc_locate_stdlib; "-stdlib", Arg.String set_stdlib, doc_stdlib; + "-c", Arg.Set create_object_file, doc_object_file; "-s", Arg.String set_simulation_node, doc_sim; "-assert", Arg.String add_assert, doc_assert; "-nopervasives", Arg.Unit set_no_pervasives, doc_no_pervasives; diff --git a/compiler/main/mls2obc.ml b/compiler/main/mls2obc.ml index 84bcb8f..2cb683f 100644 --- a/compiler/main/mls2obc.ml +++ b/compiler/main/mls2obc.ml @@ -13,32 +13,24 @@ open Names open Ident open Signature open Obc +open Types open Control open Static let gen_obj_name n = (shortname n) ^ "_mem" ^ (gen_symbol ()) -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 = 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 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) + | [] -> e | idx :: l -> mk_lhs (Larray (lhs_of_idx_list e l, idx)) let array_elt_of_exp idx e = - match e with - | Const (Carray (_, c)) -> - Const c + match e.e_desc with + | Econst ({ se_desc = Sarray_power (c, _) }) -> + mk_exp (Econst c) | _ -> - Lhs (Array(lhs_of_exp e, Lhs idx)) + mk_lhs_exp (Larray(lhs_of_exp e, mk_exp (Elhs idx))) (** Creates the expression that checks that the indices in idx_list are in the bounds. If idx_list=[e1;..;ep] @@ -46,34 +38,18 @@ let array_elt_of_exp idx e = 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], [n] -> + mk_exp (Eop (op_from_string "<", + [ idx; mk_exp (Econst n)])) | (idx :: idx_list, n :: bounds) -> - Op (op_from_string "&", - [ Op (op_from_string "<", [ idx; Const (Cint n) ]); - bound_check_expr idx_list bounds ]) + let e = mk_exp (Eop (op_from_string "<", + [idx; mk_exp (Econst n)])) in + mk_exp (Eop (op_from_string "&", + [e; 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_static_exp const_env n) - | Types.Tprod ty -> assert false - -let rec translate_const const_env = function - | Minils.Sint v -> Cint v - | Minils.Sbool v -> Cbool v - | Minils.Sfloat v -> Cfloat v - | Minils.Sconstructor c -> Cconstr c - | Minils.Sarray_power (n, c) -> - Carray_power (int_of_static_exp const_env n, translate_const const_env c) - | Minils.Sarray se_list -> - Carray (List.map (translate_const const_env) se_list) - | Minils.Stuple se_list -> - Ctuple (List.map (translate_const const_env) se_list) - | Minils.Svar n -> simplify const_env (SVar n) +let reinit o = + Acall ([], o, Mreset, []) let rec translate_pat map = function | Minils.Evarpat x -> [ var_from_name map x ] @@ -82,64 +58,66 @@ let rec translate_pat map = function pat_list [] (* [translate e = c] *) -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.Ecall ({ Minils.op_name = n; Minils.op_kind = Minils.Efun }, - e_list, _) when Mls_utils.is_op n -> - 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)) +let rec translate map (m, si, j, s) e = + let desc = match e.Minils.e_desc with + | Minils.Econst v -> Econst v + | Minils.Evar n -> Elhs (var_from_name map n) + | Minils.Eapp ({ Minils.a_op = Minils.Efun n }, + e_list, _) when Mls_utils.is_op n -> + Eop (n, List.map (translate map (m, si, j, s)) e_list) + | Minils.Ewhen (e, _, _) -> + let e = translate map (m, si, j, s) e in + e.e_desc | Minils.Estruct f_e_list -> let type_name = (match e.Minils.e_ty with - | Types.Tid name -> name + | 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))) + (fun (f, e) -> (f, (translate 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_static_exp const_env e))) idx - in - Lhs (lhs_of_idx_list (lhs_of_exp e) idx_list) + in Estruct (type_name, f_e_list) + | Minils.Eapp ({ Minils.a_op = Minils.Efield; + Minils.a_params = [{ se_desc = Sconstructor f }] }, + [e], _) -> + let e = translate map (m, si, j, s) e in + Elhs (mk_lhs (Lfield (lhs_of_exp e, f))) + (*Array operators*) + | Minils.Eapp ({ Minils.a_op = Minils.Earray }, e_list, _) -> + Earray (List.map (translate map (m, si, j, s)) e_list) + | Minils.Eapp ({ Minils.a_op = Minils.Eselect; + Minils.a_params = idx }, [e], _) -> + let e = translate map (m, si, j, s) e in + let idx_list = List.map (fun idx -> mk_exp (Econst idx)) idx in + Elhs (lhs_of_idx_list (lhs_of_exp e) idx_list) | _ -> (*Minils_printer.print_exp stdout e; flush stdout;*) assert false + in + mk_exp ~ty:e.Minils.e_ty desc (* [translate pat act = si, j, d, s] *) -and translate_act const_env map ((m, _, _, _) as context) pat +and translate_act 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) + | Minils.Etuplepat p_list, + Minils.Eapp ({ Minils.a_op = Minils.Etuple }, act_list, _) -> + List.flatten (List.map2 (translate_act map context) p_list act_list) | pat, Minils.Ewhen (e, _, _) -> - translate_act const_env map context pat e + translate_act 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) + [Acase (mk_exp (Elhs lhs), + translate_c_act_list map context pat c_act_list)] | Minils.Evarpat n, _ -> - Assgn (var_from_name map n, translate const_env map context act) + [Aassgn (var_from_name map n, translate map context act)] | _ -> (*Minils_printer.print_exp stdout act;*) assert false -and translate_c_act_list const_env map context pat c_act_list = +and translate_c_act_list 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 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.eq_lhs = pat; Minils.eq_rhs = e } +let rec translate_eq 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 @@ -148,195 +126,200 @@ let rec translate_eq const_env map { Minils.eq_lhs = pat; Minils.eq_rhs = e } let si = (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 + (Aassgn (x, + mk_exp (Econst c))) :: si) in let m = (n, ty) :: m in - let action = Assgn (var_from_name map n, - translate const_env map (m, si, j, s) e) + let action = Aassgn (var_from_name map n, + translate 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 - | Minils.Efun) as op_kind }, + | pat, Minils.Eapp ({ Minils.a_op = Minils.Efun n | Minils.Enode n; + Minils.a_params = params } as app, e_list, r) -> let name_list = translate_pat map pat in - let c_list = List.map (translate const_env map (m, si, j, s)) e_list in - let o = gen_obj_name n in + let c_list = List.map (translate map (m, si, j, s)) e_list in + let o = Oobj (gen_obj_name n) in let si = - (match op_kind with - | Minils.Enode -> (Reinit o) :: si - | Minils.Efun -> si) in - let params = List.map (int_of_static_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 = (match r, op_kind with - | Some r, Minils.Enode -> + (match app.Minils.a_op with + | Minils.Enode _ -> (reinit o) :: si + | Minils.Efun _ -> si) in + let j = (o, n, None) :: j in + let action = Acall (name_list, o, Mstep, c_list) in + let s = (match r, app.Minils.a_op with + | Some r, Minils.Enode _ -> let ra = control map (Minils.Con (ck, Name "true", r)) - (Reinit o) in + (reinit o) in ra :: (control map ck action) :: s | _, _ -> (control map ck action) :: s) in m, si, j, s - | Minils.Etuplepat p_list, Minils.Etuple act_list -> + | Minils.Etuplepat p_list, + Minils.Eapp({ Minils.a_op = Minils.Etuple }, act_list, _) -> List.fold_right2 (fun pat e -> - translate_eq const_env map + translate_eq map (Minils.mk_equation pat e)) p_list act_list (m, si, j, s) - | Minils.Evarpat x, Minils.Efield_update (f, e1, e2) -> + | Minils.Evarpat x, + Minils.Eapp ({ Minils.a_op = Minils.Efield_update; + Minils.a_params = [{ se_desc = Sconstructor 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 copy = Aassgn (x, translate map (m, si, j, s) e1) in let action = - Assgn (Field (x, f), translate const_env map (m, si, j, s) e2) + Aassgn (mk_lhs (Lfield (x, f)), translate 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_static_exp const_env idx1 in - let idx2 = int_of_static_exp const_env idx2 in + Minils.Eapp ({ Minils.a_op = Minils.Eselect_slice; + Minils.a_params = [idx1; idx2] }, [e], _) -> 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 e = translate map (m, si, j, s) e in + let idx = mk_exp (Eop (op_from_string "+", + [mk_evar cpt; + mk_exp (Econst idx1) ])) in + (* bound = (idx2 - idx1) + 1*) + let bound = + mk_static_exp (Sop(op_from_string "+", + [ mk_static_exp (Sint 1); + mk_static_exp (Sop (op_from_string "-", + [idx2;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)))) + Afor (cpt, mk_static_exp (Sint 0), bound, + [Aassgn (mk_lhs (Larray (var_from_name map x, mk_evar cpt)), + mk_lhs_exp (Larray (lhs_of_exp e, idx)))] ) in m, si, j, (control map ck action) :: s | Minils.Evarpat x, - Minils.Earray_op (Minils.Eselect_dyn (idx, e1, e2)) -> + Minils.Eapp ({ Minils.a_op = Minils.Eselect_dyn }, e1::e2::idx, _) -> let x = var_from_name map x in let bounds = Mls_utils.bounds_list e1.Minils.e_ty in - let e1 = translate const_env map (m, si, j, s) e1 in - let bounds = List.map (int_of_static_exp const_env) bounds in - let idx = List.map (translate const_env map (m, si, j, s)) idx in + let e1 = translate map (m, si, j, s) e1 in + let idx = List.map (translate 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 + Aassgn (x, mk_exp (Elhs (lhs_of_idx_list (lhs_of_exp e1) idx))) in + let false_act = Aassgn (x, translate 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 + let action = Acase (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)) -> + Minils.Eapp ({ Minils.a_op = Minils.Eupdate; + Minils.a_params = 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_static_exp const_env se))) - idx in - let action = Assgn (lhs_of_idx_list x idx, - translate const_env map (m, si, j, s) e2) + let copy = Aassgn (x, translate map (m, si, j, s) e1) in + let idx = List.map (fun idx -> mk_exp (Econst idx)) idx in + let action = Aassgn (lhs_of_idx_list x idx, + translate 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)) -> + Minils.Eapp ({ Minils.a_op = Minils.Earray_fill; + Minils.a_params = [n] }, [e], _) -> let cpt = Ident.fresh "i" in let action = - For (cpt, 0, int_of_static_exp const_env n, - Assgn (Array (var_from_name map x, Lhs (Var cpt)), - translate const_env map (m, si, j, s) e)) + Afor (cpt, mk_static_exp (Sint 0), n, + [Aassgn (mk_lhs (Larray (var_from_name map x, + mk_evar cpt)), + translate 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)) -> + Minils.Eapp ({ Minils.a_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_static_exp const_env n1 in - let n2 = int_of_static_exp const_env n2 in + | Tarray (_, n1), Tarray (_, n2) -> + let e1 = translate map (m, si, j, s) e1 in + let e2 = translate map (m, si, j, s) e2 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 + Afor (cpt1, mk_static_exp (Sint 0), n1, + [Aassgn (mk_lhs (Larray (x, mk_evar cpt1)), + mk_lhs_exp (Larray (lhs_of_exp e1, + mk_evar cpt1)))] ) in + let idx = mk_exp (Eop (op_from_string "+", + [ mk_exp (Econst n1); mk_evar cpt2])) in let a2 = - For (cpt2, 0, n2, - Assgn (Array (x, idx), - Lhs (Array (lhs_of_exp e2, Lhs (Var cpt2))))) + Afor (cpt2, static_exp_of_int 0, n2, + [Aassgn (mk_lhs (Larray (x, idx)), + mk_lhs_exp (Larray (lhs_of_exp e2, + mk_evar 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)) -> + | pat, Minils.Eiterator (it, + ({ Minils.a_op = Minils.Efun f | Minils.Enode f; + Minils.a_params = params } as app), + n, e_list, reset) -> let name_list = translate_pat map pat in let c_list = - List.map (translate const_env map (m, si, j, s)) e_list in - let o = gen_obj_name f in - let n = int_of_static_exp const_env n in - let si = - (match k with - | Minils.Efun -> si - | Minils.Enode -> (Reinit o) :: si) in - let params = List.map (int_of_static_exp const_env) params in - let j = (o, (encode_longname_params f params), n) :: j in + List.map (translate map (m, si, j, s)) e_list in let x = Ident.fresh "i" in - let action = - translate_iterator const_env map it x name_list o n c_list in + let o = Oarray (gen_obj_name f, mk_lhs (Lvar x)) in + let si = + (match app.Minils.a_op with + | Minils.Efun _ -> si + | Minils.Enode _ -> (reinit o) :: si) in + let j = (o, f, Some n) :: j in + let action = translate_iterator map it x name_list o n c_list in + let action = List.map (control map ck) action 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 ) + (match reset, app.Minils.a_op with + | Some r, Minils.Enode _ -> + (control map (Minils.Con (ck, Name "true", r)) (reinit o)) :: + action @ s + | _, _ -> action @ s) in (m, si, j, 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 action = translate_act map (m, si, j, s) pat e in + let action = List.map (control map ck) action in + m, si, j, action @ s + +and translate_iterator map it x name_list objn n c_list = + let array_of_output name_list = + List.map (fun l -> mk_lhs (Larray (l, mk_evar x))) name_list in + let array_of_input c_list = + List.map (array_elt_of_exp (mk_lhs (Lvar x))) c_list in -and translate_iterator const_env map it x name_list o n c_list = match it with | Minils.Imap -> - let c_list = - List.map (array_elt_of_exp (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)) + let c_list = array_of_input c_list in + let name_list = array_of_output name_list in + [ Afor (x, static_exp_of_int 0, n, + [Acall (name_list, objn, Mstep, c_list)]) ] | Minils.Imapfold -> let (c_list, acc_in) = split_last c_list in - let c_list = List.map (array_elt_of_exp (Var x)) c_list in - let objn = Array_context (o, Var x) in + let c_list = array_of_input c_list 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 ]))) + let name_list = array_of_output name_list in + [Aassgn (acc_out, acc_in); + Afor (x, static_exp_of_int 0, n, + [Acall (name_list @ [ acc_out ], objn, Mstep, + c_list @ [ mk_exp (Elhs acc_out) ])] )] | Minils.Ifold -> let (c_list, acc_in) = split_last c_list in - let c_list = List.map (array_elt_of_exp (Var x)) c_list in - let objn = Array_context (o, Var x) in + let c_list = array_of_input c_list 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 ]))) + [ Aassgn (acc_out, acc_in); + Afor (x, static_exp_of_int 0, n, + [Acall (name_list, objn, Mstep, + c_list @ [ mk_exp (Elhs acc_out) ])]) ] -let translate_eq_list const_env map act_list = - List.fold_right (translate_eq const_env map) act_list ([], [], [], []) +let translate_eq_list map act_list = + List.fold_right (translate_eq map) act_list ([], [], [], []) let remove m d_list = List.filter (fun { Minils.v_ident = n } -> not (List.mem_assoc n m)) d_list @@ -344,42 +327,44 @@ let remove m d_list = let var_decl 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 obj_decl l = + List.map (fun (x, t, i) -> + { o_name = obj_call_name x; o_class = t; + o_size = i; o_loc = Location.no_location (*TODO*) }) l -let translate_var_dec const_env map l = +let translate_var_dec map l = let one_var { Minils.v_ident = x; Minils.v_type = t } = - mk_var_dec x (translate_type const_env t) + mk_var_dec x t in List.map one_var l -let translate_contract const_env map = +let translate_contract map = function - | None -> ([], [], [], [], [], []) + | 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 (m, si, j, s_list) = translate_eq_list 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 d_list = translate_var_dec map d_list in + (m, si, j, s_list, d_list) (** Returns a map, mapping variables names to the variables 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_ident = x } -> Env.add x (Var x) m) + List.fold_left + (fun m { Minils.v_ident = x } -> Env.add x (mk_lhs (Lvar x)) m) Env.empty (inputs @ outputs @ locals) in - List.fold_left (fun m x -> Env.add x (Mem x) m) m mems + List.fold_left (fun m x -> Env.add x (mk_lhs (Lmem x)) m) m mems -let translate_node_aux const_env +let translate_node { Minils.n_name = f; Minils.n_input = i_list; @@ -387,80 +372,62 @@ let translate_node_aux const_env Minils.n_local = d_list; Minils.n_equs = eq_list; Minils.n_contract = contract; - Minils.n_params = params + Minils.n_params = params; + Minils.n_loc = loc; } = let mem_vars = List.flatten (List.map Mls_utils.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 (m, si, j, s_list) = translate_eq_list subst_map eq_list in + let (m', si', j', s_list', d_list') = + translate_contract 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 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 i_list = translate_var_dec subst_map i_list in + let o_list = translate_var_dec subst_map o_list in + let d_list = translate_var_dec 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 stepm = { + m_name = Mstep; m_inputs = i_list; m_outputs = o_list; + m_locals = d_list @ d_list'; m_body = s } in + let resetm = { + m_name = Mreset; m_inputs = []; m_outputs = []; + m_locals = []; m_body = si } in + { cd_name = f; cd_mems = m; + cd_objs = j; cd_methods = [stepm; resetm]; + cd_loc = loc } -let build_params_list 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; } - 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 translate_ty_def { Minils.t_name = name; Minils.t_desc = tdesc; + Minils.t_loc = loc } = 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_name = f; f_type = ty } -> - (f, translate_type const_env ty)) - field_ty_list) - in { t_name = name; t_desc = tdesc; } + Type_struct field_ty_list + in { t_name = name; t_desc = tdesc; t_loc = loc } -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 translate_const_def { Minils.c_name = name; Minils.c_value = se; + Minils.c_type = ty; Minils.c_loc = loc } = + { c_name = name; + c_value = se; + c_type = ty; + c_loc = loc } let program { - Minils.p_pragmas = p_pragmas_list; + Minils.p_modname = p_modname; 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); - } + { + p_modname = p_modname; + p_opened = p_module_list; + p_types = List.map translate_ty_def p_type_list; + p_consts = List.map translate_const_def p_const_list; + p_defs = List.map translate_node p_node_list; + } diff --git a/compiler/minils/main/mls2seq.ml b/compiler/minils/main/mls2seq.ml index 9119565..ca1235d 100644 --- a/compiler/minils/main/mls2seq.ml +++ b/compiler/minils/main/mls2seq.ml @@ -8,51 +8,67 @@ (**************************************************************************) open Compiler_utils +open Obc +open Minils +open Misc -(** Generation of a dataflow target *) -let dataflow_target filename p target_languages = - let rec one_target = function - (* | "z3z" :: others -> - let dirname = build_path (filename ^ "_z3z") in - let dir = clean_dir dirname in - let p = Dynamic_system.program p in - if !verbose then - comment "Translation into dynamic system (Z/3Z equations)"; - Sigali.Printer.print dir p; - one_target others - | ("vhdl_df" | "vhdl") :: others -> - let dirname = build_path (filename ^ "_vhdl") in - let dir = clean_dir dirname in - let vhdl = Mls2vhdl.translate (Filename.basename filename) p in - Vhdl.print dir vhdl; - one_target others *) - | unknown_lg :: others -> unknown_lg :: one_target others - | [] -> [] in - one_target target_languages +type target_source = + | Obc + | Obc_no_params + | Minils + | Minils_no_params -(** Generation of a sequential target *) -let sequential_target filename o target_languages = - let rec one_target = function - | "java" :: others -> - let dirname = build_path filename in - let dir = clean_dir dirname in - Java.print dir o; - one_target others - | "c" :: others -> - let dirname = build_path (filename ^ "_c") in - let dir = clean_dir dirname in - let c_ast = Cmain.translate filename o in - C.output dir c_ast; - one_target others - | unknown_lg :: others -> unknown_lg :: one_target others - | [] -> [] in - one_target target_languages +type convert_fun = + | Obc_fun of (Obc.program -> unit) + | Mls_fun of (Minils.program -> unit) -(** Whole translation. *) -let targets filename df obc target_languages = - let target_languages = dataflow_target filename df target_languages in - let target_languages = sequential_target filename obc target_languages in - match target_languages with - | [] -> () - | target :: _ -> language_error target +let write_object_file p = + let filename = (filename_of_name p.Minils.p_modname)^".epo" in + let epoc = open_out_bin filename in + comment "Generating of object file"; + output_value epoc p; + close_out epoc +let write_obc_file p = + let obc_name = (filename_of_name p.Obc.p_modname)^".obc" in + let obc = open_out obc_name in + comment "Generation of Obc code"; + Obc_printer.print obc p; + close_out obc + +let targets = [ ("obc", (Obc, Obc_fun write_obc_file)); + ("epo", (Minils, Mls_fun write_object_file)); + ("c", (Obc_no_params, Obc_fun Cmain.program)); + (* ("java", (Obc, Javamain.program)); + ("vhdl", (Minils_no_params, Vhdl.program)) *)] + +let generate_target p s = + try + let source, convert_fun = List.assoc s targets in + match source, convert_fun with + | Minils, Mls_fun convert_fun -> + convert_fun p + | Obc, Obc_fun convert_fun -> + let o = Mls2obc.program p in + convert_fun o + | Minils_no_params, Mls_fun convert_fun -> + let p_list = Callgraph_mapfold.program p in + List.iter convert_fun p_list + | Obc_no_params, Obc_fun convert_fun -> + let p_list = Callgraph_mapfold.program p in + let o_list = List.map Mls2obc.program p_list in + List.iter convert_fun o_list + with + | Not_found -> language_error s + +let program p = + (* Translation into dataflow and sequential languages *) + let targets = + if !create_object_file then + ["epo"] + else + match !target_languages with + | [] -> ["obc"]; + | l -> l + in + List.iter (generate_target p) targets; diff --git a/compiler/minils/minils.ml b/compiler/minils/minils.ml index ffd118b..70505f8 100644 --- a/compiler/minils/minils.ml +++ b/compiler/minils/minils.ml @@ -16,6 +16,10 @@ open Signature open Static open Types +(** Warning: Whenever Minils ast is modified, + minils_format_version should be incremented. *) +let minils_format_version = "1" + type iterator_type = | Imap | Ifold @@ -65,7 +69,7 @@ and op = | Efield (** arg1.a_param1 *) | Efield_update (** { arg1 with a_param1 = arg2 } *) | Earray (** [ args ] *) - | Earray_fill (** [arg1^arg2] *) + | Earray_fill (** [arg1^a_param1] *) | Eselect (** arg1[a_params] *) | Eselect_slice (** arg1[a_param1..a_param2] *) | Eselect_dyn (** arg1.[arg3...] default arg2 *) @@ -124,6 +128,8 @@ type const_dec = { c_loc : location } type program = { + p_modname : name; + p_format_version : string; p_opened : name list; p_types : type_dec list; p_nodes : node_dec list; diff --git a/compiler/minils/mls_printer.ml b/compiler/minils/mls_printer.ml index 3c4513b..1490c69 100644 --- a/compiler/minils/mls_printer.ml +++ b/compiler/minils/mls_printer.ml @@ -1,4 +1,3 @@ -open Minils open Names open Ident open Types @@ -6,6 +5,7 @@ open Static open Format open Signature open Pp_tools +open Minils (** Every print_ function is boxed, that is it doesn't export break points, Exceptions are print_list* print_type_desc *) @@ -75,58 +75,61 @@ and print_every ff reset = and print_exp_desc ff = function | Evar x -> print_ident ff x - | Econstvar x -> print_name ff x - | Econst c -> print_c ff c - | Efby ((Some c), e) -> fprintf ff "@[<2>%a fby@ %a@]" print_c c print_exp e + | Econst c -> print_static_exp ff c + | Efby ((Some c), e) -> + fprintf ff "@[<2>%a fby@ %a@]" print_static_exp c print_exp e | Efby (None, e) -> fprintf ff "pre %a" print_exp e - | Ecall (op, args, reset) -> - fprintf ff "@[<2>%a@,%a%a@]" - print_op op print_exp_tuple args print_every reset + | Eapp (app, args, reset) -> + fprintf ff "@[<2>%a%a@]" + print_app (app, args) print_every reset | Ewhen (e, c, n) -> fprintf ff "@[<2>(%a@ when %a(%a))@]" print_exp e print_longname c print_ident n - | Eifthenelse (e1, e2, e3) -> - fprintf ff "@[if %a@ then %a@ else %a@]" - print_exp e1 print_exp e2 print_exp e3 | Emerge (x, tag_e_list) -> fprintf ff "@[<2>merge %a@ %a@]" print_ident x print_tag_e_list tag_e_list - | Etuple e_list -> - print_exp_tuple ff e_list - | Efield (e, field) -> - fprintf ff "%a.%a" print_exp e print_longname field - | Efield_update (f, e1, e2) -> - fprintf ff "@[<2>{%a with .%a =@ %a}@]" - print_exp e1 print_longname f print_exp e2 | Estruct f_e_list -> print_record (print_couple print_longname print_exp """ = """) ff f_e_list - | Earray e_list -> - fprintf ff "@[<2>%a@]" (print_list_r print_exp "["";""]") e_list - | Earray_op(array_op) -> print_array_op ff array_op - - - -and print_array_op ff = function - | Erepeat (n, e) -> fprintf ff "%a^%a" print_exp e print_static_exp n - | Eselect (idx, e) -> fprintf ff "%a%a" print_exp e print_index idx - | Eselect_dyn (idx, e1, e2) -> - fprintf ff "%a%a default %a" - print_exp e1 print_dyn_index idx print_exp e2 - | Eupdate (idx, e1, e2) -> - fprintf ff "@[<2>(%a with %a =@ %a)@]" - print_exp e1 print_index idx print_exp e2 - | Eselect_slice (idx1, idx2, e) -> - fprintf ff "%a[%a..%a]" - print_exp e print_static_exp idx1 print_static_exp idx2 - | Econcat (e1, e2) -> fprintf ff "@[<2>%a@ @@ %a@]" print_exp e1 print_exp e2 | Eiterator (it, f, n, e_list, r) -> fprintf ff "@[<2>(%s (%a)<<%a>>)@,%a@]%a" (iterator_to_string it) - print_op f + print_app (f, []) print_static_exp n print_exp_tuple e_list print_every r +and print_app ff (op, e_list) = + match op, e_list with + | { a_op = Eifthenelse }, [e1; e2; e3] -> + fprintf ff "@[if %a@ then %a@ else %a@]" + print_exp e1 print_exp e2 print_exp e3 + | { a_op = Earray }, e_list -> + fprintf ff "@[<2>%a@]" (print_list_r print_exp "["";""]") e_list + | { a_op = Earray_fill; a_params = [n] }, [e] -> + fprintf ff "%a^%a" print_exp e print_static_exp n + | { a_op = Eselect; a_params = idx }, [e] -> + fprintf ff "%a%a" print_exp e print_index idx + | { a_op = Eselect_dyn }, e1::e2::idx -> + fprintf ff "%a%a default %a" + print_exp e1 print_dyn_index idx print_exp e2 + | { a_op = Eupdate; a_params = idx }, [e1; e2] -> + fprintf ff "@[<2>(%a with %a =@ %a)@]" + print_exp e1 print_index idx print_exp e2 + | { a_op = Eselect_slice; a_params = [idx1; idx2] }, [e] -> + fprintf ff "%a[%a..%a]" + print_exp e print_static_exp idx1 print_static_exp idx2 + | { a_op = Econcat }, [e1; e2] -> + fprintf ff "@[<2>%a@ @@ %a@]" print_exp e1 print_exp e2 + | { a_op = Efun f | Enode f; a_params = params }, e_list -> + print_longname ff f; + print_params ff params; + print_exp_tuple ff e_list + | { a_op = Efield; a_params = [field] }, [e] -> + fprintf ff "%a.%a" print_exp e print_static_exp field + | { a_op = Efield_update; a_params = [f] }, [e1; e2] -> + fprintf ff "@[<2>{%a with .%a =@ %a}@]" + print_exp e1 print_static_exp f print_exp e2 + and print_handler ff c = fprintf ff "@[<2>%a@]" (print_couple print_longname print_exp "("" -> "")") c @@ -170,13 +173,12 @@ let print_const_dec ff c = let print_contract ff { c_local = l; c_eq = eqs; - c_assume = e_a; c_enforce = e_g; c_controllables = cl } = - fprintf ff "@[contract@\n%a%a@ assume %a;@ enforce %a@ with %a@]" + c_assume = e_a; c_enforce = e_g } = + fprintf ff "@[contract@\n%a%a@ assume %a;@ enforce %a@@]" print_local_vars l print_eqs eqs print_exp e_a print_exp e_g - print_vd_tuple cl let print_node ff diff --git a/compiler/minils/transformations/callgraph_mapfold.ml b/compiler/minils/transformations/callgraph_mapfold.ml new file mode 100644 index 0000000..6e7d65e --- /dev/null +++ b/compiler/minils/transformations/callgraph_mapfold.ml @@ -0,0 +1,215 @@ +open Names +open Types +open Misc +open Location +open Signature +open Modules +open Static +open Global_mapfold +open Mls_mapfold +open Minils + +module Error = +struct + type error = + | Enode_unbound of longname + | Evar_unbound of name + + let message loc kind = + begin match kind with + | Enode_unbound ln -> + Printf.eprintf "%aUnknown node '%s'\n" + output_location loc + (fullname ln) + | Evar_unbound n -> + Printf.eprintf "%aUnbound static var '%s'\n" + output_location loc + n + end; + raise Misc.Error +end + +type info = + { mutable opened : program NamesEnv.t; + mutable called_nodes : ((longname * static_exp list) list) LongNameEnv.t; + mutable nodes_instances : (static_exp list list) LongNameEnv.t; + mutable nodes_names : (longname * static_exp list, longname) Hashtbl.t } + +let info = + { opened = NamesEnv.empty; + called_nodes = LongNameEnv.empty; + nodes_instances = LongNameEnv.empty; + nodes_names = Hashtbl.create 100 } + +let load_object_file modname = + let name = String.uncapitalize modname in + try + let filename = Modules.findfile (name ^ ".epo") in + let ic = open_in_bin filename in + try + let p:program = input_value ic in + if p.p_format_version <> minils_format_version then ( + Printf.eprintf "The file %s was compiled with \ + an older version of the compiler.\n \ + Please recompile %s.ept first.\n" filename name; + raise Error + ); + close_in ic; + info.opened <- NamesEnv.add p.p_modname p info.opened + with + | End_of_file | Failure _ -> + close_in ic; + Printf.eprintf "Corrupted object file %s.\n\ + Please recompile %s.ept first.\n" filename name; + raise Error + with + | Modules.Cannot_find_file(filename) -> + Printf.eprintf "Cannot find the object file '%s'.\n" + filename; + raise Error + +let node_by_longname ln = + match ln with + | Modname { qual = q; id = id } -> + if not (NamesEnv.mem q info.opened) then + load_object_file q; + (try + let p = NamesEnv.find q info.opened in + List.find (fun n -> n.n_name = id) p.p_nodes + with + Not_found -> Error.message no_location (Error.Enode_unbound ln)) + | _ -> assert false + +let collect_node_calls ln = + let edesc funs acc ed = match ed with + | Eapp ({ a_op = (Enode ln | Efun ln); a_params = params }, _, _) -> + ed, (ln, params)::acc + | _ -> raise Misc.Fallback + in + let funs = { Mls_mapfold.mls_funs_default with + edesc = edesc } in + let n = node_by_longname ln in + let _, acc = Mls_mapfold.node_dec funs [] n in + acc + +let called_nodes ln = + if not (LongNameEnv.mem ln info.called_nodes) then ( + let called = collect_node_calls ln in + info.called_nodes <- LongNameEnv.add ln called info.called_nodes; + called + ) else + LongNameEnv.find ln info.called_nodes + +let add_node_instance ln params = + if LongNameEnv.mem ln info.nodes_instances then + info.nodes_instances <- LongNameEnv.add ln + (params::(LongNameEnv.find ln info.nodes_instances)) info.nodes_instances + else + info.nodes_instances <- LongNameEnv.add ln [params] info.nodes_instances + +let get_node_instances ln = + try + LongNameEnv.find ln info.nodes_instances + with + Not_found -> [] + +let node_for_params_call ln params = + match params with + | [] -> ln + | _ -> Hashtbl.find info.nodes_names (ln,params) + +let build env params_names params_values = + List.fold_left2 (fun m { p_name = n } v -> NamesEnv.add n v m) + env params_names params_values + +module Instantiate = +struct + let static_exp funs m se = match se.se_desc with + | Svar ln -> + let se = (match ln with + | Name n -> + (try NamesEnv.find n m + with Not_found -> + Error.message no_location (Error.Evar_unbound n)) + | Modname _ -> se) in + se, m + | _ -> raise Misc.Fallback + + let edesc funs m ed = + let ed, _ = Mls_mapfold.edesc funs m ed in + let ed = match ed with + | Eapp ({ a_op = Efun ln; a_params = params } as app, e_list, r) -> + Eapp ({ app with a_op = Efun (node_for_params_call ln params); + a_params = [] }, e_list, r) + | Eapp ({ a_op = Enode ln; a_params = params } as app, e_list, r) -> + Eapp ({ app with a_op = Enode (node_for_params_call ln params); + a_params = [] }, e_list, r) + | _ -> ed + in ed, m + + let generate_new_name ln params = + match params with + | [] -> ln + | _ -> + (match ln with + | Modname { qual = q; id = id } -> + let new_ln = + Modname { qual = q; + id = id ^ (Ident.name (Ident.fresh "")) } in + Hashtbl.add info.nodes_names (ln, params) new_ln; + new_ln + | _ -> assert false) + + let node_dec_instance modname n params = + let global_funs = { global_funs_default with + static_exp = static_exp } in + let funs = { Mls_mapfold.mls_funs_default with + edesc = edesc; + global_funs = global_funs } in + let m = build NamesEnv.empty n.n_params params in + let n, _ = Mls_mapfold.node_dec_it funs m n in + + let ln = Modname { qual = modname; id = n.n_name } in + let { info = node_sig } = find_value ln in + let node_sig, _ = Global_mapfold.node_it global_funs m node_sig in + let ln = generate_new_name ln params in + Modules.add_value_by_longname ln node_sig; + n + + let node_dec modname n = + let ln = Modname { qual = modname; id = n.n_name } in + List.map (node_dec_instance modname n) (get_node_instances ln) + + let program p = + { p with p_nodes = List.flatten (List.map (node_dec p.p_modname) p.p_nodes) } +end + +let check_no_static_var se = + let static_exp_desc funs acc sed = match sed with + | Svar (Name n) -> Error.message se.se_loc (Error.Evar_unbound n) + | _ -> raise Misc.Fallback + in + let funs = { Global_mapfold.global_funs_default with + static_exp_desc = static_exp_desc } in + ignore (Global_mapfold.static_exp_it funs false se) + + +let rec call_node (ln, params) = + let n = node_by_longname ln in + let m = build NamesEnv.empty n.n_params params in + let params = List.map (simplify m) params in + List.iter check_no_static_var params; + add_node_instance ln params; + + let call_list = called_nodes ln in + let call_list = List.map + (fun (ln, p) -> ln, List.map (static_exp_subst m) p) call_list in + List.iter call_node call_list + +let program p = + let main_nodes = List.filter (fun n -> is_empty n.n_params) p.p_nodes in + let main_nodes = List.map (fun n -> (longname n.n_name, [])) main_nodes in + info.opened <- NamesEnv.add p.p_modname p NamesEnv.empty; + List.iter call_node main_nodes; + let p_list = NamesEnv.fold (fun _ p l -> p::l) info.opened [] in + List.map Instantiate.program p_list diff --git a/compiler/obc/c/cgen.ml b/compiler/obc/c/cgen.ml index da2d768..8bba4a9 100644 --- a/compiler/obc/c/cgen.ml +++ b/compiler/obc/c/cgen.ml @@ -330,11 +330,6 @@ and clhs_of_exp var_env exp = match exp.e_desc with (** We were passed an expression that is not translatable to a valid C lhs?!*) | _ -> invalid_arg "clhs_of_exp: argument not a Var, Mem or Field" -let obj_call_name o = - match o with - | Oobj obj - | Oarray (obj, _) -> obj - let rec assoc_obj instance obj_env = match obj_env with | [] -> raise Not_found @@ -644,7 +639,8 @@ let decls_of_type_decl otd = Cty_ptr Cty_char, [("x", Cty_id name); ("buf", Cty_ptr Cty_char)])] | Type_struct fl -> - let decls = List.map (fun (n,ty) -> n, ctype_of_otype ty) fl in + let decls = List.map (fun f -> f.Signature.f_name, + ctype_of_otype f.Signature.f_type) fl in [Cdecl_struct (otd.t_name, decls)];; (** Translates an Obc type declaration to its C counterpart. *) @@ -686,7 +682,8 @@ let cdefs_and_cdecls_of_type_decl otd = [Cdecl_enum (otd.t_name, nl); cdecl_of_cfundef of_string_fun; cdecl_of_cfundef to_string_fun]) | Type_struct fl -> - let decls = List.map (fun (n,ty) -> n, ctype_of_otype ty) fl in + let decls = List.map (fun f -> f.Signature.f_name, + ctype_of_otype f.Signature.f_type) fl in let decl = Cdecl_struct (otd.t_name, decls) in ([], [decl]) diff --git a/compiler/obc/c/cmain.ml b/compiler/obc/c/cmain.ml index c0ced7b..4f9262c 100644 --- a/compiler/obc/c/cmain.ml +++ b/compiler/obc/c/cmain.ml @@ -13,12 +13,14 @@ open Misc open Names open Ident open Obc +open Types open Modules open Signature open C open Cgen open Location open Printf +open Compiler_utils (** {1 Main C function generation} *) @@ -27,23 +29,24 @@ let step_counter = Ident.fresh "step_c" and max_step = Ident.fresh "step_max" let assert_node_res cd = - if List.length cd.step.inp > 0 then + let stepm = find_step_method cd in + if List.length stepm.m_inputs > 0 then (Printf.eprintf "Cannot generate run-time check for node %s with inputs.\n" - cd.cl_id; + cd.cd_name; exit 1); - if (match cd.step.out with - | [{ v_type = Tbool; }] -> false + if (match stepm.m_outputs with + | [{ v_type = Tid nbool; }] when nbool = Initial.pbool -> false | _ -> true) then (Printf.eprintf "Cannot generate run-time check for node %s with non-boolean output.\n" - cd.cl_id; + cd.cd_name; exit 1); let mem = - (name (Ident.fresh ("mem_for_" ^ cd.cl_id)), Cty_id (cd.cl_id ^ "_mem")) + (name (Ident.fresh ("mem_for_" ^ cd.cd_name)), Cty_id (cd.cd_name ^ "_mem")) and out = - (name (Ident.fresh ("out_for_" ^ cd.cl_id)), Cty_id (cd.cl_id ^ "_out")) in + (name (Ident.fresh ("out_for_" ^ cd.cd_name)), Cty_id (cd.cd_name ^ "_out")) in let reset_i = - Cfun_call (cd.cl_id ^ "_reset", [Caddrof (Cvar (fst mem))]) in + Cfun_call (cd.cd_name ^ "_reset", [Caddrof (Cvar (fst mem))]) in let step_i = (* step(&out, &mem); @@ -52,17 +55,17 @@ let assert_node_res cd = return 1; } *) - let outn = Ident.name ((List.hd cd.step.out).v_ident) in + let outn = Ident.name ((List.hd stepm.m_outputs).v_ident) in Csblock { var_decls = []; block_body = [ - Csexpr (Cfun_call (cd.cl_id ^ "_step", + Csexpr (Cfun_call (cd.cd_name ^ "_step", [Caddrof (Cvar (fst out)); Caddrof (Cvar (fst mem))])); Cif (Cuop ("!", Clhs (Cfield (Cvar (fst out), outn))), [Csexpr (Cfun_call ("printf", - [Cconst (Cstrlit ("Node \\\"" ^ cd.cl_id + [Cconst (Cstrlit ("Node \\\"" ^ cd.cd_name ^ "\\\" failed at step" ^ " %d.\\n")); Clhs (Cvar (name step_counter))])); @@ -79,15 +82,18 @@ let assert_node_res cd = let main_def_of_class_def cd = let format_for_type ty = match ty with | Tarray _ -> assert false - | Tint | Tbool -> "%d" - | Tfloat -> "%f" + | Types.Tid id when id = Initial.pfloat -> "%f" + | Types.Tid id when id = Initial.pint -> "%d" + | Types.Tid id when id = Initial.pbool -> "%d" | Tid ((Name sid) | Modname { id = sid }) -> "%s" in (** Does reading type [ty] need a buffer? When it is the case, [need_buf_for_ty] also returns the type's name. *) let need_buf_for_ty ty = match ty with | Tarray _ -> assert false - | Tint | Tfloat | Tbool -> None + | Types.Tid id when id = Initial.pfloat -> None + | Types.Tid id when id = Initial.pint -> None + | Types.Tid id when id = Initial.pbool -> None | Tid (Name sid | Modname { id = sid; }) -> Some sid in let cprint_string s = Csexpr (Cfun_call ("printf", [Cconst (Cstrlit s)])) in @@ -98,7 +104,7 @@ let main_def_of_class_def cd = let iter_var = Ident.name (Ident.fresh "i") in let lhs = Carray (lhs, Clhs (Cvar iter_var)) in let (reads, bufs) = read_lhs_of_ty lhs ty in - ([Cfor (iter_var, 0, n, reads)], bufs) + ([Cfor (iter_var, 0, int_of_static_exp n, reads)], bufs) | _ -> let rec mk_prompt lhs = match lhs with | Cvar vn -> (vn, []) @@ -134,8 +140,9 @@ let main_def_of_class_def cd = let iter_var = Ident.name (Ident.fresh "i") in let lhs = Carray (lhs, Clhs (Cvar iter_var)) in let (reads, bufs) = write_lhs_of_ty lhs ty in - ([cprint_string "[ "; Cfor (iter_var, 0, n, reads); cprint_string "]"], - bufs) + ([cprint_string "[ "; + Cfor (iter_var, 0, int_of_static_exp n, reads); + cprint_string "]"], bufs) | _ -> let varn = Ident.name (Ident.fresh "buf") in let format_s = format_for_type ty in @@ -152,24 +159,25 @@ let main_def_of_class_def cd = | None -> [] | Some id -> [(varn, Cty_arr (20, Cty_char))]) in + let stepm = find_step_method cd in let (scanf_calls, scanf_decls) = let read_lhs_of_ty_for_vd vd = read_lhs_of_ty (Cvar (Ident.name vd.v_ident)) vd.v_type in - split (map read_lhs_of_ty_for_vd cd.step.inp) in + split (map read_lhs_of_ty_for_vd stepm.m_inputs) in let (printf_calls, printf_decls) = let write_lhs_of_ty_for_vd vd = let (stm, vars) = write_lhs_of_ty (Cfield (Cvar "res", name vd.v_ident)) vd.v_type in (cprint_string "=> " :: stm, vars) in - split (map write_lhs_of_ty_for_vd cd.step.out) in + split (map write_lhs_of_ty_for_vd stepm.m_outputs) in let printf_calls = List.concat printf_calls in - let cinp = cvarlist_of_ovarlist cd.step.inp in - let cout = ["res", (Cty_id (cd.cl_id ^ "_out"))] in + let cinp = cvarlist_of_ovarlist stepm.m_inputs in + let cout = ["res", (Cty_id (cd.cd_name ^ "_out"))] in let varlist = - ("mem", Cty_id (cd.cl_id ^ "_mem")) + ("mem", Cty_id (cd.cd_name ^ "_mem")) :: cinp @ cout @ concat scanf_decls @@ -180,9 +188,9 @@ let main_def_of_class_def cd = let step_l = let funcall = let args = - map (fun vd -> Clhs (Cvar (name vd.v_ident))) cd.step.inp + map (fun vd -> Clhs (Cvar (name vd.v_ident))) stepm.m_inputs @ [Caddrof (Cvar "res"); Caddrof (Cvar "mem")] in - Cfun_call (cd.cl_id ^ "_step", args) in + Cfun_call (cd.cd_name ^ "_step", args) in concat scanf_calls @ [Csexpr funcall] @ printf_calls @@ -191,7 +199,7 @@ let main_def_of_class_def cd = (** Do not forget to initialize memory via reset. *) let rst_i = - Csexpr (Cfun_call (cd.cl_id ^ "_reset", [Caddrof (Cvar "mem")])) in + Csexpr (Cfun_call (cd.cd_name ^ "_reset", [Caddrof (Cvar "mem")])) in (varlist, rst_i, step_l) @@ -244,7 +252,7 @@ let mk_main p = match (!Misc.simulation_node, !Misc.assert_nodes) with | (None, []) -> [] | (_, n_names) -> let find_class n = - try List.find (fun cd -> cd.cl_id = n) p.o_defs + try List.find (fun cd -> cd.cd_name = n) p.p_defs with Not_found -> Printf.eprintf "Unknown node %s.\n" n; exit 1 in @@ -278,3 +286,10 @@ let translate name prog = global_name := String.capitalize modname; (global_file_header modname prog) :: (mk_main prog) @ (cfile_list_of_oprog modname prog) + +let program p = + let filename = filename_of_name p.p_modname in + let dirname = build_path (filename ^ "_c") in + let dir = clean_dir dirname in + let c_ast = translate filename p in + C.output dir c_ast diff --git a/compiler/obc/control.ml b/compiler/obc/control.ml index be42e6c..f00a8fd 100644 --- a/compiler/obc/control.ml +++ b/compiler/obc/control.ml @@ -34,7 +34,7 @@ let rec control map ck s = | Cvar { contents = Clink ck } -> control map ck s | Con(ck, c, n) -> let x = var_from_name map n in - control map ck [Acase(mk_exp (Elhs x), [(c, s)])] + control map ck (Acase(mk_exp (Elhs x), [(c, [s])])) let is_deadcode = function | Aassgn (lhs, e) -> diff --git a/compiler/obc/java/javamain.ml b/compiler/obc/java/javamain.ml new file mode 100644 index 0000000..e83e6c5 --- /dev/null +++ b/compiler/obc/java/javamain.ml @@ -0,0 +1,6 @@ + +let program p = + let filename = filename_of_module p in + let dirname = build_path filename in + let dir = clean_dir dirname in + Java.print dir o diff --git a/compiler/obc/obc.ml b/compiler/obc/obc.ml index 49da569..5657199 100644 --- a/compiler/obc/obc.ml +++ b/compiler/obc/obc.ml @@ -12,6 +12,7 @@ open Misc open Names open Ident open Types +open Signature open Location type class_name = name @@ -27,11 +28,12 @@ type type_dec = and tdesc = | Type_abs | Type_enum of name list - | Type_struct of (name * ty) list + | Type_struct of structure type const_dec = { c_name : name; c_value : static_exp; + c_type : ty; c_loc : location } type lhs = { l_desc : lhs_desc; l_ty : ty; l_loc : location } @@ -94,7 +96,8 @@ type class_def = cd_loc : location } type program = - { p_opened : name list; + { p_modname : name; + p_opened : name list; p_types : type_dec list; p_consts : const_dec list; p_defs : class_def list } @@ -108,6 +111,13 @@ let mk_exp ?(ty=invalid_type) ?(loc=no_location) desc = let mk_lhs ?(ty=invalid_type) ?(loc=no_location) desc = { l_desc = desc; l_ty = ty; l_loc = loc } +let mk_lhs_exp ?(ty=invalid_type) desc = + let lhs = mk_lhs ~ty:ty desc in + mk_exp ~ty:ty (Elhs lhs) + +let mk_evar id = + mk_exp (Elhs (mk_lhs (Lvar id))) + let rec var_name x = match x.l_desc with | Lvar x -> x @@ -128,7 +138,7 @@ let rec vd_find n = function | vd::l -> if vd.v_ident = n then vd else vd_find n l -let lhs_of_exp = function +let lhs_of_exp e = match e.e_desc with | Elhs l -> l | _ -> assert false @@ -136,3 +146,9 @@ let find_step_method cd = List.find (fun m -> m.m_name = Mstep) cd.cd_methods let find_reset_method cd = List.find (fun m -> m.m_name = Mreset) cd.cd_methods + +let obj_call_name o = + match o with + | Oobj obj + | Oarray (obj, _) -> obj + diff --git a/compiler/obc/obc_printer.ml b/compiler/obc/obc_printer.ml index d83094d..2038935 100644 --- a/compiler/obc/obc_printer.ml +++ b/compiler/obc/obc_printer.ml @@ -152,7 +152,7 @@ let print_type_def ff { t_name = name; t_desc = tdesc } = fprintf ff "@[type %s = " name; fprintf ff "@["; print_list - (fun ff (field, ty) -> + (fun ff { Signature.f_name = field; Signature.f_type = ty } -> print_name ff field; fprintf ff ": "; print_type ff ty) "{" ";" "}" ff f_ty_list; diff --git a/compiler/utilities/global/compiler_utils.ml b/compiler/utilities/global/compiler_utils.ml index 7a39327..a7e9cba 100644 --- a/compiler/utilities/global/compiler_utils.ml +++ b/compiler/utilities/global/compiler_utils.ml @@ -8,6 +8,7 @@ (**************************************************************************) open Misc open Location +open Minils let lexical_error err loc = Printf.eprintf "%aIllegal character.\n" output_location loc; @@ -49,6 +50,9 @@ let build_path suf = | None -> suf | Some path -> Filename.concat path suf +let filename_of_name n = + n + let clean_dir dir = if Sys.file_exists dir && Sys.is_directory dir then begin @@ -67,6 +71,7 @@ and doc_version = "\t\tThe version of the compiler" and doc_print_types = "\t\t\tPrint types" and doc_include = "\t\tAdd to the list of include directories" and doc_stdlib = "\t\tDirectory for the standard library" +and doc_object_file = "\t\tOnly generate a .epo object file" and doc_sim = "\t\tCreate simulation for node " and doc_locate_stdlib = "\t\tLocate standard libray" and doc_no_pervasives = "\tDo not load the pervasives module" diff --git a/compiler/utilities/misc.ml b/compiler/utilities/misc.ml index b5b2389..afa4043 100644 --- a/compiler/utilities/misc.ml +++ b/compiler/utilities/misc.ml @@ -55,6 +55,8 @@ let set_simulation_node s = simulation := true; simulation_node := Some s +let create_object_file = ref false + (* Target languages list for code generation *) let target_languages : string list ref = ref [] diff --git a/compiler/utilities/misc.mli b/compiler/utilities/misc.mli index da9734e..379c1c5 100644 --- a/compiler/utilities/misc.mli +++ b/compiler/utilities/misc.mli @@ -52,6 +52,9 @@ val simulation_node : string option ref (* Set the simulation mode on *) val set_simulation_node : string -> unit +(* If it is true, the compiler will only generate an object file (.epo). + Otherwise, it will generate obc code and possibily other targets.*) +val create_object_file : bool ref (* List of target languages *) val target_languages : string list ref (* Add target language to the list *)