From a8215c80838617a2b4e4086553c3b62b98caf1fd Mon Sep 17 00:00:00 2001 From: Leonard Gerard Date: Mon, 9 May 2011 19:32:12 +0200 Subject: [PATCH] compile ! nearly all tests passed. --- compiler/global/clocks.ml | 35 ++- compiler/global/global_printer.ml | 4 +- compiler/global/idents.ml | 1 + compiler/global/idents.mli | 5 +- compiler/global/signature.ml | 13 +- compiler/heptagon/hept_utils.ml | 5 +- compiler/heptagon/heptagon.ml | 82 +----- compiler/heptagon/parsing/hept_parser.mly | 28 +- compiler/heptagon/parsing/hept_parsetree.ml | 26 +- compiler/heptagon/parsing/hept_scoping.ml | 72 +++-- compiler/heptagon/transformations/switch.ml | 2 +- compiler/main/hept2mls.ml | 39 +-- compiler/main/mls2obc.ml | 4 +- compiler/minils/analysis/clocking.ml | 278 +++++++++--------- compiler/minils/minils.ml | 23 +- compiler/minils/mls_mapfold.ml | 4 +- compiler/minils/mls_printer.ml | 16 +- compiler/minils/mls_utils.ml | 22 +- .../minils/transformations/normalize_mem.ml | 3 +- 19 files changed, 339 insertions(+), 323 deletions(-) diff --git a/compiler/global/clocks.ml b/compiler/global/clocks.ml index e818cc5..04bbf50 100644 --- a/compiler/global/clocks.ml +++ b/compiler/global/clocks.ml @@ -38,6 +38,16 @@ let gen_index () = (incr index; !index) (** returns a new clock variable *) let fresh_clock () = Cvar { contents = Cindex (gen_index ()); } +(** returns a new clock type corresponding to the data type [ty] *) +let rec fresh_ct ty = match ty with + | Tprod ty_list -> + (match ty_list with + | [] -> Ck (fresh_clock()) + | _ -> Cprod (List.map fresh_ct ty_list)) + | Tarray (t, _) -> fresh_ct t + | Tid _ | Tinvalid -> Ck (fresh_clock()) + + (** returns the canonic (short) representant of a [ck] and update it to this value. *) let rec ck_repr ck = match ck with @@ -90,19 +100,26 @@ and unify_list t1_list t2_list = with _ -> raise Unify -let rec skeleton ck = function +let prod ck_l = match ck_l with + | [ck] -> Ck ck + | _ -> Cprod (List.map (fun ck -> Ck ck) ck_l) + +(* +let rec tuple ck = function | Tprod ty_list -> (match ty_list with | [] -> Ck ck - | _ -> Cprod (List.map (skeleton ck) ty_list)) - | Tarray (t, _) -> skeleton ck t + | _ -> Cprod (List.map (tuple ck) ty_list)) + | Tarray (t, _) -> tuple ck t | Tid _ | Tinvalid -> Ck ck +*) +(* +let max ck_1 ck_2 = match ck_repr ck_1, ck_reprck_2 with + | -(* TODO here it implicitely says that the base clock is Cbase - and that all tuple is on Cbase *) -let ckofct = function | Ck ck -> ck_repr ck | Cprod _ -> Cbase - - - +let rec optim_base_ck base_ck ct = match ct with + | Ck ck -> + | Cprod c_l -> +*) diff --git a/compiler/global/global_printer.ml b/compiler/global/global_printer.ml index fb97c35..a102d24 100644 --- a/compiler/global/global_printer.ml +++ b/compiler/global/global_printer.ml @@ -149,8 +149,8 @@ let print_ident ff id = Format.fprintf ff "%s" (name id) | Cvar { contents = Cindex _ } -> fprintf ff "base" | Cvar { contents = Clink ck } -> print_ck ff ck -let rec print_clock ff = function +let rec print_ct ff = function | Ck ck -> print_ck ff ck | Cprod ct_list -> - fprintf ff "@[<2>(%a)@]" (print_list_r print_clock """ *""") ct_list + fprintf ff "@[<2>(%a)@]" (print_list_r print_ct """ *""") ct_list diff --git a/compiler/global/idents.ml b/compiler/global/idents.ml index 318ef35..c7e3344 100644 --- a/compiler/global/idents.ml +++ b/compiler/global/idents.ml @@ -138,6 +138,7 @@ let ident_of_name s = let id = { num = !num; source = s; is_generated = false } in UniqueNames.assign_name id; id +let source_name id = id.source let name id = UniqueNames.name id let enter_node n = UniqueNames.enter_node n diff --git a/compiler/global/idents.mli b/compiler/global/idents.mli index 571c665..bc38346 100644 --- a/compiler/global/idents.mli +++ b/compiler/global/idents.mli @@ -18,6 +18,9 @@ val ident_compare : ident -> ident -> int (** Get the full name of an identifier (it is guaranteed to be unique) *) val name : ident -> string +(** Get the source name of an identifier (useful when dealing with signatures *) +val source_name : ident -> string + (** [gen_fresh pass_name kind_to_string kind] generate a fresh ident with a sweet [name]. It should be used to define a [fresh] function specific to a pass. *) @@ -27,7 +30,7 @@ val gen_fresh : string -> ('a -> string) -> 'a -> ident generates a fresh ident with a sweet [name] *) val gen_var : string -> string -> ident -(** [ident_of_name n] returns an identifier corresponding +(** [ident_of_name n] returns an fresh identifier corresponding to a _source_ variable (do not use it for generated variables). *) val ident_of_name : string -> ident diff --git a/compiler/global/signature.ml b/compiler/global/signature.ml index c040ab1..2a57f94 100644 --- a/compiler/global/signature.ml +++ b/compiler/global/signature.ml @@ -9,12 +9,15 @@ (* global data in the symbol tables *) open Names open Types -open Clocks (** Warning: Whenever these types are modified, interface_format_version should be incremented. *) let interface_format_version = "30" +type ck = + | Cbase + | Con of ck * constructor_name * name + (** Node argument : inputs and outputs *) type arg = { a_name : name option; @@ -50,6 +53,14 @@ type type_def = type const_def = { c_type : ty; c_value : static_exp } +let rec ck_to_sck ck = + let ck = Clocks.ck_repr ck in + match ck with + | Clocks.Cbase -> Cbase + | Clocks.Con (ck,c,x) -> Con(ck_to_sck ck, c, Idents.source_name x) + | _ -> Misc.internal_error "Signature couldn't translate ck" 1 + + let names_of_arg_list l = List.map (fun ad -> ad.a_name) l let types_of_arg_list l = List.map (fun ad -> ad.a_type) l diff --git a/compiler/heptagon/hept_utils.ml b/compiler/heptagon/hept_utils.ml index 8953540..919c449 100644 --- a/compiler/heptagon/hept_utils.ml +++ b/compiler/heptagon/hept_utils.ml @@ -19,9 +19,10 @@ open Initial open Heptagon (* Helper functions to create AST. *) -let mk_exp desc ?(ct_annot = Clocks.invalid_clock) ?(loc = no_location) ty = +(* TODO : After switch, all mk_exp should take care of level_ck *) +let mk_exp desc ?(level_ck = Cbase) ?(ct_annot = None) ?(loc = no_location) ty = { e_desc = desc; e_ty = ty; e_ct_annot = ct_annot; - e_base_ck = Cbase; e_loc = loc; } + e_level_ck = level_ck; e_loc = loc; } let mk_app ?(params=[]) ?(unsafe=false) op = { a_op = op; a_params = params; a_unsafe = unsafe } diff --git a/compiler/heptagon/heptagon.ml b/compiler/heptagon/heptagon.ml index 663ed71..4df0227 100644 --- a/compiler/heptagon/heptagon.ml +++ b/compiler/heptagon/heptagon.ml @@ -29,8 +29,8 @@ type iterator_type = type exp = { e_desc : desc; e_ty : ty; - e_ct_annot : ct; - e_base_ck : ck; + e_ct_annot : ct option; (* exists when a source annotation exists *) + e_level_ck : ck; (* set by the switch pass, represents the base activation of the expression *) e_loc : location } and desc = @@ -188,82 +188,4 @@ and interface_desc = | Itypedef of type_dec | Iconstdef of const_dec | Isignature of signature -(* -(* Helper functions to create AST. *) -let mk_exp desc ?(ct_annot = Clocks.invalid_clock) ?(loc = no_location) ty = - { e_desc = desc; e_ty = ty; e_ct_annot = ct_annot; - e_base_ck = Cbase; e_loc = loc; } -let mk_app ?(params=[]) ?(unsafe=false) op = - { a_op = op; a_params = params; a_unsafe = unsafe } - -let mk_op_app ?(params=[]) ?(unsafe=false) ?(reset=None) op args = - Eapp(mk_app ~params:params ~unsafe:unsafe op, args, reset) - -let mk_type_dec name desc = - { t_name = name; t_desc = desc; t_loc = no_location; } - -let mk_equation stateful desc = - { eq_desc = desc; eq_stateful = stateful; eq_loc = no_location; } - -let mk_var_dec ?(last = Var) ?(clock = fresh_clock()) name ty = - { v_ident = name; v_type = ty; v_clock = clock; - v_last = last; v_loc = no_location } - -let mk_block stateful ?(defnames = Env.empty) ?(locals = []) eqs = - { b_local = locals; b_equs = eqs; b_defnames = defnames; - b_stateful = stateful; b_loc = no_location; } - -let dfalse = - mk_exp (Econst (mk_static_bool false)) (Tid Initial.pbool) -let dtrue = - mk_exp (Econst (mk_static_bool true)) (Tid Initial.pbool) - -let mk_ifthenelse e1 e2 e3 = - { e3 with e_desc = mk_op_app Eifthenelse [e1; e2; e3] } - -let mk_simple_equation stateful pat e = - mk_equation stateful (Eeq(pat, e)) - -let mk_switch_equation stateful e l = - mk_equation stateful (Eswitch (e, l)) - - -let mk_signature name ins outs stateful params loc = - { sig_name = name; - sig_inputs = ins; - sig_stateful = stateful; - sig_outputs = outs; - sig_params = params; - sig_loc = loc } - -let mk_node - ?(input = []) ?(output = []) ?(contract = None) ?(local = []) - ?(stateful = true) ?(loc = no_location) ?(param = []) ?(constraints = []) - name block = - { n_name = name; - n_stateful = stateful; - n_input = input; - n_output = output; - n_contract = contract; - n_block = block; - n_loc = loc; - n_params = param; - n_params_constraints = constraints } - -(** @return the set of variables defined in [pat]. *) -let vars_pat pat = - let rec _vars_pat locals acc = function - | Evarpat x -> - if (IdentSet.mem x locals) or (IdentSet.mem x acc) - then acc - else IdentSet.add x acc - | Etuplepat pat_list -> List.fold_left (_vars_pat locals) acc pat_list - in _vars_pat IdentSet.empty IdentSet.empty pat - -(** @return whether an object of name [n] belongs to - a list of [var_dec]. *) -let rec vd_mem n = function - | [] -> false - | vd::l -> vd.v_ident = n or (vd_mem n l) -*) diff --git a/compiler/heptagon/parsing/hept_parser.mly b/compiler/heptagon/parsing/hept_parser.mly index 7e97d28..9db93af 100644 --- a/compiler/heptagon/parsing/hept_parser.mly +++ b/compiler/heptagon/parsing/hept_parser.mly @@ -193,8 +193,8 @@ nonmt_params: ; param: - | ident_list COLON ty_ident - { List.map (fun id -> mk_var_dec id $3 Var (Loc($startpos,$endpos))) $1 } + | idl=ident_list COLON ty=ty_ident ck=ck + { List.map (fun id -> mk_var_dec id ty ck Var (Loc($startpos,$endpos))) idl } ; out_params: @@ -248,12 +248,12 @@ loc_params: var_last: - | ident_list COLON ty_ident - { List.map (fun id -> mk_var_dec id $3 Var (Loc($startpos,$endpos))) $1 } - | LAST IDENT COLON ty_ident EQUAL exp - { [ mk_var_dec $2 $4 (Last(Some($6))) (Loc($startpos,$endpos)) ] } - | LAST IDENT COLON ty_ident - { [ mk_var_dec $2 $4 (Last(None)) (Loc($startpos,$endpos)) ] } + | idl=ident_list COLON ty=ty_ident ck=ck + { List.map (fun id -> mk_var_dec id ty ck Var (Loc($startpos,$endpos))) idl } + | LAST id=IDENT COLON ty=ty_ident ck=ck EQUAL e=exp + { [ mk_var_dec id ty ck (Last(Some(e))) (Loc($startpos,$endpos)) ] } + | LAST id=IDENT COLON ty=ty_ident ck=ck + { [ mk_var_dec id ty ck (Last(None)) (Loc($startpos,$endpos)) ] } ; ident_list: @@ -268,9 +268,13 @@ ty_ident: { Tarray ($1, $3) } ; +ck: + | /*empty */ { None } + | ON ck=on_ck { Some ck } + on_ck: - | /*empty */ { Cbase } - | b=on_ck ON c=constructor_or_bool LPAREN x=IDENT RPAREN { Con (b,c,x) } + | c=constructor_or_bool LPAREN x=IDENT RPAREN { Con(Cbase,c,x) } + | b=on_ck ON c=constructor_or_bool LPAREN x=IDENT RPAREN { Con(b,c,x) } equs: | /* empty */ { [] } @@ -630,8 +634,8 @@ nonmt_params_signature: ; param_signature: - | IDENT COLON ty_ident ck=on_ck { mk_arg (Some $1) $3 ck } - | ty_ident ck=on_ck { mk_arg None $1 ck } + | IDENT COLON ty_ident ck=ck { mk_arg (Some $1) $3 ck } + | ty_ident ck=ck { mk_arg None $1 ck } ; %% diff --git a/compiler/heptagon/parsing/hept_parsetree.ml b/compiler/heptagon/parsing/hept_parsetree.ml index 68a26c2..6394fb9 100644 --- a/compiler/heptagon/parsing/hept_parsetree.ml +++ b/compiler/heptagon/parsing/hept_parsetree.ml @@ -65,11 +65,14 @@ and ck = | Cbase | Con of ck * constructor_name * var_name +and ct = + | Ck of ck + | Cprod of ct list and exp = - { e_desc : edesc; - e_ct_annot : Clocks.ct; - e_loc : location } + { e_desc : edesc; + e_ct_annot : ct option ; + e_loc : location } and edesc = | Econst of static_exp @@ -144,10 +147,11 @@ and present_handler = p_block : block; } and var_dec = - { v_name : var_name; - v_type : ty; - v_last : last; - v_loc : location; } + { v_name : var_name; + v_type : ty; + v_clock : ck option; + v_last : last; + v_loc : location; } and last = Var | Last of exp option @@ -198,7 +202,7 @@ and program_desc = type arg = { a_type : ty; - a_clock : ck; + a_clock : ck option; a_name : var_name option } type signature = @@ -223,7 +227,7 @@ and interface_desc = (* {3 Helper functions to create AST} *) -let mk_exp desc ?(ct_annot = Clocks.invalid_clock) loc = +let mk_exp desc ?(ct_annot = None) loc = { e_desc = desc; e_ct_annot = ct_annot; e_loc = loc } let mk_app op params = @@ -256,8 +260,8 @@ let mk_equation desc loc = let mk_interface_decl desc loc = { interf_desc = desc; interf_loc = loc } -let mk_var_dec name ty last loc = - { v_name = name; v_type = ty; +let mk_var_dec name ty ck last loc = + { v_name = name; v_type = ty; v_clock = ck; v_last = last; v_loc = loc } let mk_block locals eqs loc = diff --git a/compiler/heptagon/parsing/hept_scoping.ml b/compiler/heptagon/parsing/hept_scoping.ml index 6ba7b7a..b50c3f0 100644 --- a/compiler/heptagon/parsing/hept_scoping.ml +++ b/compiler/heptagon/parsing/hept_scoping.ml @@ -233,13 +233,25 @@ let rec translate_type loc ty = with | ScopingError err -> message loc err +let rec translate_some_clock loc env ck = match ck with + | None -> Clocks.fresh_clock() + | Some(ck) -> translate_clock loc env ck + +and translate_clock loc env ck = match ck with + | Cbase -> Clocks.Cbase + | Con(ck,c,x) -> Clocks.Con(translate_clock loc env ck, qualify_constrs c, Rename.var loc env x) + +let rec translate_ct loc env ct = match ct with + | Ck ck -> Clocks.Ck (translate_clock loc env ck) + | Cprod c_l -> Clocks.Cprod (List.map (translate_ct loc env) c_l) + let rec translate_exp env e = try { Heptagon.e_desc = translate_desc e.e_loc env e.e_desc; Heptagon.e_ty = Types.invalid_type; - Heptagon.e_base_ck = Clocks.Cbase; - Heptagon.e_ct_annot = e.e_ct_annot; + Heptagon.e_level_ck = Clocks.Cbase; + Heptagon.e_ct_annot = Misc.optional (translate_ct e.e_loc env) e.e_ct_annot; Heptagon.e_loc = e.e_loc } with ScopingError(error) -> message e.e_loc error @@ -374,9 +386,10 @@ and translate_var_dec env vd = { Heptagon.v_ident = Rename.var vd.v_loc env vd.v_name; Heptagon.v_type = translate_type vd.v_loc vd.v_type; Heptagon.v_last = translate_last vd.v_last; - Heptagon.v_clock = Clocks.fresh_clock(); (* TODO add clock annotations *) + Heptagon.v_clock = translate_some_clock vd.v_loc env vd.v_clock; Heptagon.v_loc = vd.v_loc } +(** [env] should contain the declared variables prior to this translation *) and translate_vd_list env = List.map (translate_var_dec env) @@ -398,26 +411,27 @@ let params_of_var_decs = (translate_type vd.v_loc vd.v_type)) let args_of_var_decs = - List.map (fun vd -> Signature.mk_arg - (Some vd.v_name) - (translate_type vd.v_loc vd.v_type) - Clocks.Cbase) (* before clocking and without annotations, default choice.*) + (* before the clocking the clock is wrong in the signature *) + List.map (fun vd -> Signature.mk_arg (Some (Idents.source_name vd.Heptagon.v_ident)) + vd.Heptagon.v_type Signature.Cbase) + let translate_node node = let n = current_qual node.n_name in Idents.enter_node n; - (* Inputs and outputs define the initial local env *) - let env0 = Rename.append Rename.empty (node.n_input @ node.n_output) in let params = params_of_var_decs node.n_params in - let inputs = translate_vd_list env0 node.n_input in + let input_env = Rename.append Rename.empty (node.n_input) in + (* inputs should refer only to inputs *) + let inputs = translate_vd_list input_env node.n_input in + (* Inputs and outputs define the initial local env *) + let env0 = Rename.append input_env node.n_output in let outputs = translate_vd_list env0 node.n_output in let b, env = translate_block env0 node.n_block in - let contract = - Misc.optional (translate_contract env) node.n_contract in - (* the env of the block is used in the contract translation *) + (* the env of the block is used in the contract translation *) + let contract = Misc.optional (translate_contract env) node.n_contract in (* add the node signature to the environment *) - let i = args_of_var_decs node.n_input in - let o = args_of_var_decs node.n_output in + let i = args_of_var_decs inputs in + let o = args_of_var_decs outputs in let p = params_of_var_decs node.n_params in add_value n (Signature.mk_node i o node.n_stateful p); { Heptagon.n_name = n; @@ -483,14 +497,30 @@ let translate_program p = Heptagon.p_desc = desc; } let translate_signature s = - let translate_arg a = - Signature.mk_arg a.a_name - (translate_type s.sig_loc a.a_type) - (translate_clock s.sig_loc a.a_clock)) + (* helper functions, having [env] as being the list of existing var names *) + let rec append env sa_l = match sa_l with + | [] -> env + | sa::sa_l -> match sa.a_name with + | None -> append env sa_l + | Some x -> append (x::env) sa_l + and translate_some_clock loc env ck = match ck with + | None -> Signature.Cbase + | Some ck -> translate_clock loc env ck + and translate_clock loc env ck = match ck with + | Cbase -> Signature.Cbase + | Con(ck,c,x) -> + if not (List.mem x env) + then message loc (Evar_unbound x) + else Signature.Con(translate_clock loc env ck, qualify_constrs c, x) + and translate_arg env a = + Signature.mk_arg a.a_name (translate_type s.sig_loc a.a_type) + (translate_some_clock s.sig_loc env a.a_clock) in let n = current_qual s.sig_name in - let i = List.map translate_arg s.sig_inputs in - let o = List.map translate_arg s.sig_outputs in + let env = append [] s.sig_inputs in + let i = List.map (translate_arg env) s.sig_inputs in + let env = append env s.sig_outputs in + let o = List.map (translate_arg env) s.sig_outputs in let p = params_of_var_decs s.sig_params in add_value n (Signature.mk_node i o s.sig_stateful p); mk_signature n i o s.sig_stateful p s.sig_loc diff --git a/compiler/heptagon/transformations/switch.ml b/compiler/heptagon/transformations/switch.ml index 6d58091..b3ac085 100644 --- a/compiler/heptagon/transformations/switch.ml +++ b/compiler/heptagon/transformations/switch.ml @@ -105,7 +105,7 @@ let current_level env = match env with (** Set the base clock of an expression to the current level of the [env] *) let annot_exp e env = - { e with e_base_ck = current_level env } + { e with e_level_ck = current_level env } end diff --git a/compiler/main/hept2mls.ml b/compiler/main/hept2mls.ml index 984291a..13db8cf 100644 --- a/compiler/main/hept2mls.ml +++ b/compiler/main/hept2mls.ml @@ -104,45 +104,46 @@ let rec translate_extvalue e = mk_extvalue (Wfield (translate_extvalue e, fn)) | _ -> Error.message e.Heptagon.e_loc Error.Enormalization -let translate - ({ Heptagon.e_desc = desc; Heptagon.e_ty = ty; - Heptagon.e_loc = loc } as e) = - let mk_exp = mk_exp ~loc:loc in - match desc with +let translate ({ Heptagon.e_desc = desc; Heptagon.e_ty = ty; Heptagon.e_level_ck = b_ck; + Heptagon.e_ct_annot = a_ct; Heptagon.e_loc = loc } as e) = + let desc = match desc with | Heptagon.Econst _ | Heptagon.Evar _ | Heptagon.Ewhen _ | Heptagon.Eapp({ Heptagon.a_op = Heptagon.Efield }, _, _) -> let w = translate_extvalue e in - mk_exp ty (Eextvalue w) + Eextvalue w | Heptagon.Epre(None, e) -> - mk_exp ty (Efby(None, translate_extvalue e)) + Efby(None, translate_extvalue e) | Heptagon.Epre(Some c, e) -> - mk_exp ty (Efby(Some c, translate_extvalue e)) + Efby(Some c, translate_extvalue e) | Heptagon.Efby ({ Heptagon.e_desc = Heptagon.Econst c }, e) -> - mk_exp ty (Efby(Some c, translate_extvalue e)) + Efby(Some c, translate_extvalue e) | Heptagon.Estruct f_e_list -> let f_e_list = List.map (fun (f, e) -> (f, translate_extvalue e)) f_e_list in - mk_exp ty (Estruct f_e_list) + Estruct f_e_list | Heptagon.Eapp({ Heptagon.a_op = Heptagon.Earrow }, _, _) -> Error.message loc Error.Eunsupported_language_construct | Heptagon.Eapp(app, e_list, reset) -> - mk_exp ty (Eapp (translate_app app, - List.map translate_extvalue e_list, - translate_reset reset)) + Eapp (translate_app app, List.map translate_extvalue e_list, translate_reset reset) | Heptagon.Eiterator(it, app, n, pe_list, e_list, reset) -> - mk_exp ty - (Eiterator (translate_iterator_type it, + Eiterator (translate_iterator_type it, translate_app app, n, List.map translate_extvalue pe_list, List.map translate_extvalue e_list, - translate_reset reset)) + translate_reset reset) | Heptagon.Efby _ | Heptagon.Elast _ -> Error.message loc Error.Eunsupported_language_construct | Heptagon.Emerge (x, c_e_list) -> - mk_exp ty (Emerge (x, List.map (fun (c,e)-> c, translate_extvalue e) c_e_list)) + Emerge (x, List.map (fun (c,e)-> c, translate_extvalue e) c_e_list) + in + match a_ct with + | None -> mk_exp b_ck ty ~loc:loc desc + | Some ct -> mk_exp b_ck ty ~ct:ct ~loc:loc desc + + let rec translate_pat = function | Heptagon.Evarpat(n) -> Evarpat n @@ -167,8 +168,8 @@ let translate_contract contract = Heptagon.c_controllables = l_c } -> Some { c_local = List.map translate_var v; c_eq = List.map translate_eq eq_list; - c_assume = translate e_a; - c_enforce = translate e_g; + c_assume = translate_extvalue e_a; + c_enforce = translate_extvalue e_g; c_controllables = List.map translate_var l_c } let node n = diff --git a/compiler/main/mls2obc.ml b/compiler/main/mls2obc.ml index 007315b..83e09c6 100644 --- a/compiler/main/mls2obc.ml +++ b/compiler/main/mls2obc.ml @@ -11,12 +11,12 @@ open Misc open Names open Idents -open Clocks open Signature open Obc open Obc_utils open Obc_mapfold open Types +open Clocks open Static open Initial @@ -361,7 +361,7 @@ let empty_call_context = None [v] var decs *) let rec translate_eq map call_context { Minils.eq_lhs = pat; Minils.eq_rhs = e } (v, si, j, s) = - let { Minils.e_desc = desc; Minils.e_ck = ck; Minils.e_loc = loc } = e in + let { Minils.e_desc = desc; Minils.e_base_ck = ck; Minils.e_loc = loc } = e in match (pat, desc) with | Minils.Evarpat n, Minils.Efby (opt_c, e) -> let x = var_from_name map n in diff --git a/compiler/minils/analysis/clocking.ml b/compiler/minils/analysis/clocking.ml index 3b3d774..fef4416 100644 --- a/compiler/minils/analysis/clocking.ml +++ b/compiler/minils/analysis/clocking.ml @@ -8,9 +8,19 @@ (**************************************************************************) (* clock checking *) +(* v_clock is expected to contain correct clocks before entering here : + either explicit with Cbase representing the node activation clock + or fresh_clock() for unannoted variables. + Idem for e_ct : if explicit, it represents a clock annotation. + Unification is done on this mutable fields. + e_base_ck is set according to node signatures. + + *) + open Misc open Idents open Minils +open Global_printer open Mls_printer open Signature open Types @@ -19,139 +29,152 @@ open Location open Format (** Error Kind *) -type error_kind = | Etypeclash of ct * ct +type error_kind = | Etypeclash of ct * ct | Eclockclash of ck * ck | Edefclock let error_message loc = function | Etypeclash (actual_ct, expected_ct) -> Format.eprintf "%aClock Clash: this expression has clock %a,@\n\ but is expected to have clock %a.@." print_location loc - print_clock actual_ct - print_clock expected_ct; + print_ct actual_ct + print_ct expected_ct; + raise Errors.Error + | Eclockclash (actual_ck, expected_ck) -> + Format.eprintf "%aClock Clash: this value has clock %a,@\n\ + but is exprected to have clock %a.@." + print_location loc + print_ck actual_ck + print_ck expected_ck; + raise Errors.Error + | Edefclock -> + Format.eprintf "%aArguments defining clocks should be given as names@." + print_location loc; raise Errors.Error -let typ_of_name h x = Env.find x h +let ck_of_name h x = Env.find x h let rec typing_extvalue h w = - let ct = match w.w_desc with - | Wconst se -> skeleton (fresh_clock ()) se.se_ty - | Wvar x -> Ck (typ_of_name h x) + let ck = match w.w_desc with + | Wconst se -> fresh_clock() + | Wvar x -> ck_of_name h x | Wwhen (w1, c, n) -> - let ck_n = typ_of_name h n in - (expect h (skeleton ck_n w1.w_ty) w1; skeleton (Con (ck_n, c, n)) w1.w_ty) + let ck_n = ck_of_name h n in + expect_extvalue h ck_n w1; + Con (ck_n, c, n) | Wfield (w1, f) -> - let ck = fresh_clock () in - let ct = skeleton ck w1.w_ty in (expect h (Ck ck) w1; ct) - in (w.w_ck <- ckofct ct; ct) + typing_extvalue h w1 + in + w.w_ck <- ck; + ck -and expect h expected_ty e = - let actual_ty = typing_extvalue h e in - try unify actual_ty expected_ty +and expect_extvalue h expected_ck e = + let actual_ck = typing_extvalue h e in + try unify_ck actual_ck expected_ck with | Unify -> eprintf "%a : " print_extvalue e; - error_message e.w_loc (Etypeclash (actual_ty, expected_ty)) + error_message e.w_loc (Eclockclash (actual_ck, expected_ck)) -let rec typing h e = - let ct = match e.e_desc with - | Eextvalue w -> typing_extvalue h w - | Efby (_, e) -> typing_extvalue h e - | Eapp({a_op = op}, args, r) -> - let ck = match r with - | None -> fresh_clock () - | Some(reset) -> typ_of_name h reset in - typing_op op args h e ck - (* Typed exactly as a fun or a node... *) - | Eiterator (_, _, _, pargs, args, r) -> - let ck = match r with - | None -> fresh_clock() - | Some(reset) -> typ_of_name h reset - in - List.iter (expect h (Ck ck)) pargs; - List.iter (expect h (Ck ck)) args; - skeleton ck e.e_ty - | Emerge (n, c_e_list) -> - let ck_c = typ_of_name h n in - (typing_c_e_list h ck_c n c_e_list; skeleton ck_c e.e_ty) +let rec typing_pat h = function + | Evarpat x -> Ck (ck_of_name h x) + | Etuplepat pat_list -> Cprod (List.map (typing_pat h) pat_list) + + +let typing_app h base pat op w_list = match op with + | Earray_fill | Eselect | Eselect_dyn | Eselect_trunc | Eupdate | Eequal + | Eselect_slice | Econcat | Earray | Efield_update | Eifthenelse -> + List.iter (expect_extvalue h base) w_list; + Ck base + | ( Efun f | Enode f) -> + let node = Modules.find_value f in + let pat_id_list = Mls_utils.ident_list_of_pat pat in + let rec build_env a_l v_l env = match a_l, v_l with + | [],[] -> env + | a::a_l, v::v_l -> (match a.a_name with + | None -> build_env a_l v_l env + | Some n -> build_env a_l v_l ((n,v)::env)) + | _ -> Misc.internal_error "Clocking, non matching signature" 2 + in + let env_pat = build_env node.node_outputs pat_id_list [] in + let env_args = build_env node.node_inputs w_list [] in + (* implement with Cbase as base, replace name dep by ident dep *) + let rec sigck_to_ck sck = match sck with + | Signature.Cbase -> base + | Signature.Con (sck,c,x) -> + (* find x in the envs : *) + let id = try List.assoc x env_pat + with Not_found -> + try + let w = List.assoc x env_args in + (match w.w_desc with + | Wvar id -> id + | _ -> error_message w.w_loc Edefclock) + with Not_found -> + Misc.internal_error "Clocking, non matching signature" 3 + in + Clocks.Con (sigck_to_ck sck, c, id) + in + List.iter2 (fun a w -> expect_extvalue h (sigck_to_ck a.a_clock) w) node.node_inputs w_list; + Clocks.prod (List.map (fun a -> sigck_to_ck a.a_clock) node.node_outputs) + + +let typing_eq h { eq_lhs = pat; eq_rhs = e } = + (* typing the expression *) + let ct,base = match e.e_desc with + | Eextvalue w + | Efby (_, w) -> + let ck = typing_extvalue h w in + Ck ck, ck + | Emerge (x, c_e_list) -> + let ck = ck_of_name h x in + List.iter (fun (c,e) -> expect_extvalue h (Con (ck,c,x)) e) c_e_list; + Ck ck, ck | Estruct l -> let ck = fresh_clock () in - (List.iter - (fun (_, e) -> let ct = skeleton ck e.w_ty in expect h ct e) l; - Ck ck) - in (e.e_ck <- ckofct ct; ct) + List.iter (fun (_, e) -> expect_extvalue h ck e) l; + Ck ck, ck + | Eapp({a_op = op}, args, r) -> + let ck_r = match r with + | None -> fresh_clock () + | Some(reset) -> ck_of_name h reset in + let ct = typing_app h ck_r pat op args in + ct, ck_r + | Eiterator (_, _, _, pargs, args, r) -> + (* Typed exactly as a fun or a node... *) + let ck_r = match r with + | None -> fresh_clock() + | Some(reset) -> ck_of_name h reset + in + List.iter (expect_extvalue h ck_r) pargs; + List.iter (expect_extvalue h ck_r) args; + (*TODO*) + Ck ck_r, ck_r + in + e.e_base_ck <- base; + begin + try unify ct e.e_ct + with Unify -> + eprintf "Incoherent clock annotation.@\n"; + error_message e.e_loc (Etypeclash (ct,e.e_ct)) + end; + e.e_ct <- ct; + (* typing the full equation *) + let pat_ct = typing_pat h pat in + begin + try unify ct pat_ct + with Unify -> + eprintf "Incoherent clock between right and left side of the equation@\n"; + error_message e.e_loc (Etypeclash (ct, pat_ct)) + end -and typing_op op e_list h e ck = match op with - | (Eequal | Efun _ | Enode _) -> (*LA*) - List.iter (fun e -> expect h (skeleton ck e.w_ty) e) e_list; - skeleton ck e.e_ty - | Eifthenelse -> - let e1, e2, e3 = assert_3 e_list in - let ct = skeleton ck e.e_ty - in (expect h (Ck ck) e1; expect h ct e2; expect h ct e3; ct) - | Efield_update -> - let e1, e2 = assert_2 e_list in - let ct = skeleton ck e.e_ty - in (expect h (Ck ck) e1; expect h ct e2; ct) - | Earray -> - (List.iter (expect h (Ck ck)) e_list; skeleton ck e.e_ty) - | Earray_fill -> let e = assert_1 e_list in typing_extvalue h e - | Eselect -> let e = assert_1 e_list in typing_extvalue h e - | Eselect_dyn -> (* TODO defe not treated ? *) - let e1, defe, idx = assert_2min e_list in - let ct = skeleton ck e1.w_ty - in (List.iter (expect h ct) (e1::defe::idx); ct) - | Eselect_trunc -> - let e1, idx = assert_1min e_list in - let ct = skeleton ck e1.w_ty - in (List.iter (expect h ct) (e1::idx); ct) - | Eupdate -> - let e1, e2, idx = assert_2min e_list in - let ct = skeleton ck e.e_ty - in (expect h (Ck ck) e1; expect h ct e2; List.iter (expect h ct) idx; ct) - | Eselect_slice -> let e = assert_1 e_list in typing_extvalue h e - | Econcat -> - let e1, e2 = assert_2 e_list in - let ct = skeleton ck e.e_ty - in (expect h (Ck ck) e1; expect h ct e2; ct) -and typing_c_e_list h ck_c n c_e_list = - let rec typrec = - function - | [] -> () - | (c, e) :: c_e_list -> - (expect h (skeleton (Con (ck_c, c, n)) e.w_ty) e; typrec c_e_list) - in typrec c_e_list +let typing_eqs h eq_list = List.iter (typing_eq h) eq_list -let expect_exp h expected_ty e = - let actual_ty = typing h e in - try unify actual_ty expected_ty - with - | Unify -> eprintf "%a : " print_exp e; - error_message e.e_loc (Etypeclash (actual_ty, expected_ty)) +let append_env h vds = + List.fold_left (fun h { v_ident = n; v_clock = ck } -> Env.add n ck h) h vds -let rec typing_pat h = - function - | Evarpat x -> Ck (typ_of_name h x) - | Etuplepat pat_list -> Cprod (List.map (typing_pat h) pat_list) -let typing_eqs h eq_list = (*TODO FIXME*) - let typing_eq { eq_lhs = pat; eq_rhs = e } = - let ty_pat = typing_pat h pat in - (try expect_exp h ty_pat e with - | Errors.Error -> (* DEBUG *) - Format.eprintf "Complete expression: %a@\nClock pattern: %a@." - Mls_printer.print_exp e - Mls_printer.print_clock ty_pat; - raise Errors.Error) - in List.iter typing_eq eq_list - -let build h dec = - List.fold_left (fun h { v_ident = n } -> Env.add n (fresh_clock ()) h) h dec - -let sbuild h dec base = - List.fold_left (fun h { v_ident = n } -> Env.add n base h) h dec - -let typing_contract h contract base = +let typing_contract h contract = match contract with | None -> h | Some { c_local = l_list; @@ -159,32 +182,25 @@ let typing_contract h contract base = c_assume = e_a; c_enforce = e_g; c_controllables = c_list } -> - let h' = build h l_list in + let h' = append_env h l_list in (* assumption *) (* property *) typing_eqs h' eq_list; - expect_exp h' (Ck base) e_a; - expect_exp h' (Ck base) e_g; - sbuild h c_list base + expect_extvalue h' Cbase e_a; + expect_extvalue h' Cbase e_g; + append_env h c_list -let typing_node ({ n_input = i_list; - n_output = o_list; - n_contract = contract; - n_local = l_list; - n_equs = eq_list - } as node) = - let base = Cbase in - let h = sbuild Env.empty i_list base in - let h = sbuild h o_list base in - let h = typing_contract h contract base in - let h = build h l_list in - (typing_eqs h eq_list; - (*update clock info in variables descriptions *) - let set_clock vd = { vd with v_clock = ck_repr (Env.find vd.v_ident h) } in - { (node) with - n_input = List.map set_clock i_list; - n_output = List.map set_clock o_list; - n_local = List.map set_clock l_list }) +let typing_node node = + let h = append_env Env.empty node.n_input in + let h = append_env h node.n_output in + let h = typing_contract h node.n_contract in + let h = append_env h node.n_local in + (typing_eqs h node.n_equs; + (*update clock info in variables descriptions *) + let set_clock vd = { vd with v_clock = ck_repr (Env.find vd.v_ident h) } in + { 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 }) let program p = let program_desc pd = match pd with diff --git a/compiler/minils/minils.ml b/compiler/minils/minils.ml index fbd38ea..4ffcd2f 100644 --- a/compiler/minils/minils.ml +++ b/compiler/minils/minils.ml @@ -46,16 +46,18 @@ and extvalue = { w_loc : location } and extvalue_desc = - | Wconst of static_exp + | Wconst of static_exp (*no tuple*) | Wvar of var_ident | Wfield of extvalue * field_name | Wwhen of extvalue * constructor_name * var_ident (** extvalue when Constructor(ident) *) and exp = { - e_desc : edesc; - mutable e_ck: ck; - e_ty : ty; - e_loc : location } + 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_loc : location } and edesc = | Eextvalue of extvalue @@ -107,8 +109,8 @@ type var_dec = { v_loc : location } type contract = { - c_assume : exp; - c_enforce : exp; + c_assume : extvalue; + c_enforce : extvalue; c_controllables : var_dec list; c_local : var_dec list; c_eq : eq list } @@ -119,8 +121,6 @@ type node_dec = { n_input : var_dec list; n_output : var_dec list; n_contract : contract option; - (* GD: inglorious hack for controller call - mutable n_controller_call : var_ident list * var_ident list; *) n_local : var_dec list; n_equs : eq list; n_loc : location; @@ -150,9 +150,8 @@ let mk_extvalue ~ty ?(clock = fresh_clock()) ?(loc = no_location) desc = { w_desc = desc; w_ty = ty; w_ck = clock; w_loc = loc } -let mk_exp ty ?(clock = fresh_clock()) ?(loc = no_location) desc = - { e_desc = desc; e_ty = ty; - e_ck = clock; e_loc = loc } +let mk_exp level_ck ty ?(ck = Cbase) ?(ct = fresh_ct ty) ?(loc = no_location) desc = + { e_desc = desc; e_ty = ty; e_level_ck = level_ck; e_base_ck = ck; e_ct = ct; e_loc = loc } let mk_var_dec ?(loc = no_location) ?(clock = fresh_clock()) ident ty = { v_ident = ident; v_type = ty; v_clock = clock; v_loc = loc } diff --git a/compiler/minils/mls_mapfold.ml b/compiler/minils/mls_mapfold.ml index 2575d0d..0cb5d02 100644 --- a/compiler/minils/mls_mapfold.ml +++ b/compiler/minils/mls_mapfold.ml @@ -136,8 +136,8 @@ and var_decs funs acc vds = mapfold (var_dec_it funs) acc vds and contract_it funs acc c = funs.contract funs acc c and contract funs acc c = - let c_assume, acc = exp_it funs acc c.c_assume in - let c_enforce, acc = exp_it funs acc c.c_enforce in + let c_assume, acc = extvalue_it funs acc c.c_assume in + let c_enforce, acc = extvalue_it funs acc c.c_enforce in let c_local, acc = var_decs_it funs acc c.c_local in let c_eq, acc = eqs_it funs acc c.c_eq in { c with diff --git a/compiler/minils/mls_printer.ml b/compiler/minils/mls_printer.ml index 40ad008..aaa28e8 100644 --- a/compiler/minils/mls_printer.ml +++ b/compiler/minils/mls_printer.ml @@ -1,11 +1,11 @@ open Misc open Names +open Signature open Idents open Types open Clocks open Static open Format -open Signature open Global_printer open Pp_tools open Minils @@ -27,7 +27,7 @@ let rec print_pat ff = function | Evarpat n -> print_ident ff n | Etuplepat pat_list -> fprintf ff "@[<2>(%a)@]" (print_list_r print_pat """,""") pat_list - +(* let rec print_ck ff = function | Cbase -> fprintf ff "base" | Con (ck, c, n) -> @@ -35,11 +35,11 @@ let rec print_ck ff = function | Cvar { contents = Cindex _ } -> fprintf ff "base" | Cvar { contents = Clink ck } -> print_ck ff ck -let rec print_clock ff = function +let rec print_ct ff = function | Ck ck -> print_ck ff ck | Cprod ct_list -> fprintf ff "@[<2>(%a)@]" (print_list_r print_clock """ *""") ct_list - +*) let print_vd ff { v_ident = n; v_type = ty; v_clock = ck } = if !Compiler_options.full_type_info then fprintf ff "%a : %a :: %a" print_ident n print_type ty print_ck ck @@ -86,7 +86,7 @@ and print_trunc_index ff idx = and print_exp ff e = if !Compiler_options.full_type_info then fprintf ff "(%a : %a :: %a)" - print_exp_desc e.e_desc print_type e.e_ty print_ck e.e_ck + print_exp_desc e.e_desc print_type e.e_ty print_ct e.e_ct else fprintf ff "%a" print_exp_desc e.e_desc and print_every ff reset = @@ -180,7 +180,7 @@ and print_tag_w_list ff tag_w_list = and print_eq ff { eq_lhs = p; eq_rhs = e } = if !Compiler_options.full_type_info then fprintf ff "@[<2>%a :: %a =@ %a@]" - print_pat p print_ck e.e_ck print_exp e + print_pat p print_ck e.e_base_ck print_exp e else fprintf ff "@[<2>%a =@ %a@]" print_pat p print_exp e @@ -207,8 +207,8 @@ let print_contract ff { c_local = l; c_eq = eqs; fprintf ff "@[contract@\n%a%a@ assume %a@ enforce %a@ with (%a)@]" print_local_vars l print_eqs eqs - print_exp e_a - print_exp e_g + print_extvalue e_a + print_extvalue e_g print_vd_tuple c diff --git a/compiler/minils/mls_utils.ml b/compiler/minils/mls_utils.ml index 6844894..99f2e98 100644 --- a/compiler/minils/mls_utils.ml +++ b/compiler/minils/mls_utils.ml @@ -46,10 +46,6 @@ let rec vd_mem n = function | [] -> false | vd::l -> vd.v_ident = n or (vd_mem n l) -(** @return a signature arguments from the vardecs *) -let args_of_var_decs vds = - List.map (fun vd -> Signature.mk_arg (Some (name vd.v_ident)) vd.v_type) vds - (** @return whether [ty] corresponds to a record type. *) let is_record_type ty = match ty with @@ -77,6 +73,10 @@ struct | Cbase | Cvar { contents = Cindex _ } -> acc | Cvar { contents = Clink ck } -> vars_ck acc ck + let rec vars_ct acc = function + | Ck ck -> vars_ck acc ck + | Cprod c_l -> List.fold_left vars_ct acc c_l + let read_extvalue read_funs (is_left, acc_init) w = (* recursive call *) let _,(_, acc) = Mls_mapfold.extvalue read_funs (is_left, acc_init) w in @@ -104,7 +104,7 @@ struct else acc | _ -> acc in - e, (is_left, vars_ck acc e.e_ck) + e, (is_left, vars_ct acc e.e_ct) let read_exp is_left acc e = let _, (_, acc) = @@ -136,9 +136,7 @@ struct let antidep { eq_rhs = e } = match e.e_desc with Efby _ -> true | _ -> false - let clock { eq_rhs = e } = match e.e_desc with - | Emerge(_, (_, e) :: _) -> e.w_ck - | _ -> e.e_ck + let clock { eq_rhs = e } = e.e_base_ck let head ck = let rec headrec ck l = @@ -191,3 +189,11 @@ module AllDep = Dep.Make let eq_find id = List.find (fun eq -> List.mem id (Vars.def [] eq)) + +let ident_list_of_pat pat = + let rec f acc pat = match pat with + | Evarpat id -> id::acc + | Etuplepat [] -> acc + | Etuplepat (pat::pat_l) -> f (f acc pat) (Etuplepat pat_l) + in + f [] pat diff --git a/compiler/minils/transformations/normalize_mem.ml b/compiler/minils/transformations/normalize_mem.ml index a54c2a5..21ecfba 100644 --- a/compiler/minils/transformations/normalize_mem.ml +++ b/compiler/minils/transformations/normalize_mem.ml @@ -22,8 +22,9 @@ let eq _ (outputs, eqs, env) eq = match eq.eq_lhs, eq.eq_rhs.e_desc with | Evarpat x, Efby _ -> if Mls_utils.vd_mem x outputs then let ty = eq.eq_rhs.e_ty in + let ck = eq.eq_rhs.e_base_ck in let x_copy = Idents.gen_var "normalize_mem" ("out_"^(Idents.name x)) in - let exp_x = mk_exp ty (Eextvalue (mk_extvalue ~ty:ty (Wvar x))) in + let exp_x = mk_exp ck ty (Eextvalue (mk_extvalue ~ty:ty (Wvar x))) in let eq_copy = { eq with eq_lhs = Evarpat x_copy; eq_rhs = exp_x } in let env = Env.add x x_copy env in eq, (outputs, eq::eq_copy::eqs, env)