From ed2642f847fa658687df9b7a363bc3f24cbeb546 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Gwena=EBl=20Delaval?= Date: Wed, 8 Dec 2010 17:32:24 +0100 Subject: [PATCH] Added controllables in every pass --- compiler/heptagon/analysis/initialization.ml | 8 +++++--- compiler/heptagon/analysis/typing.ml | 12 ++++++++---- compiler/heptagon/hept_mapfold.ml | 8 ++++++-- compiler/heptagon/parsing/hept_scoping.ml | 1 + compiler/main/hept2mls.ml | 8 ++++++-- compiler/minils/analysis/clocking.ml | 11 ++++++----- compiler/minils/minils.ml | 4 +++- 7 files changed, 35 insertions(+), 17 deletions(-) diff --git a/compiler/heptagon/analysis/initialization.ml b/compiler/heptagon/analysis/initialization.ml index 374f01a..637e73d 100644 --- a/compiler/heptagon/analysis/initialization.ml +++ b/compiler/heptagon/analysis/initialization.ml @@ -365,15 +365,17 @@ let build_initialized h vdecs = let typing_contract h contract = match contract with | None -> h - | Some { c_block = b; c_assume = e_a; - c_enforce = e_g } -> + | Some { c_block = b; + c_assume = e_a; + c_enforce = e_g; + c_controllables = c } -> let h' = build h b.b_local in typing_eqs h' b.b_equs; (* assumption *) expect h' e_a (skeleton izero e_a.e_ty); (* property *) expect h' e_g (skeleton izero e_g.e_ty); - h + build_initialized h c let typing_node { n_input = i_list; n_output = o_list; n_contract = contract; n_block = b } = diff --git a/compiler/heptagon/analysis/typing.ml b/compiler/heptagon/analysis/typing.ml index 450265d..4896927 100644 --- a/compiler/heptagon/analysis/typing.ml +++ b/compiler/heptagon/analysis/typing.ml @@ -990,7 +990,8 @@ let typing_contract const_env h contract = | None -> None,h | Some ({ c_block = b; c_assume = e_a; - c_enforce = e_g }) -> + c_enforce = e_g; + c_controllables = c }) -> let typed_b, defined_names, _ = typing_block const_env h b in (* check that the equations do not define other unexpected names *) included_env defined_names Env.empty; @@ -1000,9 +1001,12 @@ let typing_contract const_env h contract = (* property *) let typed_e_g = expect const_env h (Tid Initial.pbool) e_g in - Some { c_block = typed_b; - c_assume = typed_e_a; - c_enforce = typed_e_g }, h + let typed_c, (c_names, h) = build const_env h c in + + Some { c_block = typed_b; + c_assume = typed_e_a; + c_enforce = typed_e_g; + c_controllables = typed_c }, h let solve loc cl = try diff --git a/compiler/heptagon/hept_mapfold.ml b/compiler/heptagon/hept_mapfold.ml index 22a9722..c09078f 100644 --- a/compiler/heptagon/hept_mapfold.ml +++ b/compiler/heptagon/hept_mapfold.ml @@ -254,9 +254,13 @@ 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_block, acc = block_it funs acc c.c_block in + let c_controllables, acc = mapfold (var_dec_it funs) acc c.c_controllables in { c with - c_assume = c_assume; c_enforce = c_enforce; c_block = c_block } - , acc + c_assume = c_assume; + c_enforce = c_enforce; + c_block = c_block; + c_controllables = c_controllables }, + acc and param_it funs acc vd = funs.param funs acc vd and param funs acc vd = diff --git a/compiler/heptagon/parsing/hept_scoping.ml b/compiler/heptagon/parsing/hept_scoping.ml index a21f235..e8d66d7 100644 --- a/compiler/heptagon/parsing/hept_scoping.ml +++ b/compiler/heptagon/parsing/hept_scoping.ml @@ -364,6 +364,7 @@ let translate_contract env ct = let b, _ = translate_block env ct.c_block in { Heptagon.c_assume = translate_exp env ct.c_assume; Heptagon.c_enforce = translate_exp env ct.c_enforce; + Heptagon.c_controllables = translate_vd_list env ct.c_controllables; Heptagon.c_block = b } let params_of_var_decs = diff --git a/compiler/main/hept2mls.ml b/compiler/main/hept2mls.ml index e1c7ff0..543093e 100644 --- a/compiler/main/hept2mls.ml +++ b/compiler/main/hept2mls.ml @@ -350,7 +350,8 @@ let translate_contract env contract = | Some { Heptagon.c_block = { Heptagon.b_local = v; Heptagon.b_equs = eq_list }; Heptagon.c_assume = e_a; - Heptagon.c_enforce = e_g} -> + Heptagon.c_enforce = e_g; + Heptagon.c_controllables = l_c } -> let env' = Env.add v env in let locals = translate_locals [] v in let locals, l_eqs, s_eqs = @@ -358,10 +359,12 @@ let translate_contract env contract = let l_eqs, _ = add_locals IdentSet.empty l_eqs [] s_eqs in let e_a = translate env' e_a in let e_g = translate env' e_g in + let env = Env.add l_c env in Some { c_local = locals; c_eq = l_eqs; c_assume = e_a; - c_enforce = e_g }, + c_enforce = e_g; + c_controllables = List.map translate_var l_c }, env @@ -383,6 +386,7 @@ let node n_input = List.map translate_var i; n_output = List.map translate_var o; n_contract = contract; + n_controller_call = ([],[]); n_local = locals; n_equs = l_eqs; n_loc = loc ; diff --git a/compiler/minils/analysis/clocking.ml b/compiler/minils/analysis/clocking.ml index ffac52d..3fbe459 100644 --- a/compiler/minils/analysis/clocking.ml +++ b/compiler/minils/analysis/clocking.ml @@ -139,14 +139,15 @@ let typing_contract h contract base = | Some { c_local = l_list; c_eq = eq_list; c_assume = e_a; - c_enforce = e_g; } -> + c_enforce = e_g; + c_controllables = c_list } -> let h' = build h l_list in (* assumption *) (* property *) - (typing_eqs h' eq_list; - expect h' (Ck base) e_a; - expect h' (Ck base) e_g; - h) + typing_eqs h' eq_list; + expect h' (Ck base) e_a; + expect h' (Ck base) e_g; + sbuild h c_list base let typing_node ({ n_input = i_list; n_output = o_list; diff --git a/compiler/minils/minils.ml b/compiler/minils/minils.ml index 32ae91d..41c1a24 100644 --- a/compiler/minils/minils.ml +++ b/compiler/minils/minils.ml @@ -144,11 +144,13 @@ let mk_equation ?(loc = no_location) pat exp = let mk_node ?(input = []) ?(output = []) ?(contract = None) ?(local = []) ?(eq = []) - ?(loc = no_location) ?(param = []) ?(constraints = []) ?(pinst = []) name = + ?(loc = no_location) ?(param = []) ?(constraints = []) + ?(pinst = ([],[])) name = { n_name = name; n_input = input; n_output = output; n_contract = contract; + n_controller_call = pinst; n_local = local; n_equs = eq; n_loc = loc;