From bb0bc8bfe54318290b21c86c7586fbc98e00da74 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Gwena=EBl=20Delaval?= Date: Tue, 29 May 2012 14:14:46 +0200 Subject: [PATCH] Added local assume/guarantee Added local assume/guarantee in contracts. No syntax associated to these local asume/guarantee: internal use only. --- compiler/heptagon/analysis/causality.ml | 15 ++++++++++++--- compiler/heptagon/analysis/hept_clocking.ml | 5 +++++ compiler/heptagon/analysis/typing.ml | 6 ++++++ compiler/heptagon/hept_mapfold.ml | 4 ++++ compiler/heptagon/heptagon.ml | 2 ++ compiler/heptagon/parsing/hept_parser.mly | 2 ++ compiler/heptagon/parsing/hept_parsetree.ml | 2 ++ .../heptagon/parsing/hept_parsetree_mapfold.ml | 8 +++++++- compiler/heptagon/parsing/hept_scoping.ml | 6 +++++- compiler/heptagon/transformations/boolean.ml | 6 ++++++ compiler/heptagon/transformations/normalize.ml | 4 ++++ compiler/main/hept2mls.ml | 4 ++++ compiler/minils/analysis/clocking.ml | 4 ++++ compiler/minils/minils.ml | 4 +++- compiler/minils/mls_mapfold.ml | 9 ++++++++- 15 files changed, 74 insertions(+), 7 deletions(-) diff --git a/compiler/heptagon/analysis/causality.ml b/compiler/heptagon/analysis/causality.ml index 178ee4b..4bb057e 100644 --- a/compiler/heptagon/analysis/causality.ml +++ b/compiler/heptagon/analysis/causality.ml @@ -216,10 +216,19 @@ and typing_block { b_local = dec; b_equs = eq_list; b_loc = loc } = let typing_contract loc contract = match contract with | None -> cempty - | Some { c_block = b; c_assume = e_a; - c_enforce = e_g } -> + | Some { c_block = b; + c_assume = e_a; + c_assume_loc = e_a_loc; + c_enforce = e_g; + c_enforce_loc = e_g_loc; + } -> let teq = typing_eqs b.b_equs in - let t_contract = cseq (typing e_a) (cseq teq (typing e_g)) in + let t_contract = + cseq + (typing e_a) + (cseq (typing e_g) + (cseq (typing e_a_loc) + (cseq (typing e_g_loc) teq))) in Causal.check loc t_contract; let t_contract = clear (build b.b_local) t_contract in t_contract diff --git a/compiler/heptagon/analysis/hept_clocking.ml b/compiler/heptagon/analysis/hept_clocking.ml index 74cf95a..bac5c7f 100644 --- a/compiler/heptagon/analysis/hept_clocking.ml +++ b/compiler/heptagon/analysis/hept_clocking.ml @@ -234,12 +234,17 @@ let typing_contract h contract = | Some { c_block = b; c_assume = e_a; c_enforce = e_g; + c_assume_loc = e_a_loc; + c_enforce_loc = e_g_loc; c_controllables = c_list } -> let h' = typing_block h b in (* assumption *) expect h' (Etuplepat []) (Ck Cbase) e_a; + expect h' (Etuplepat []) (Ck Cbase) e_a_loc; (* property *) expect h' (Etuplepat []) (Ck Cbase) e_g; + expect h' (Etuplepat []) (Ck Cbase) e_g_loc; + append_env h c_list (* check signature causality and update it in the global env *) diff --git a/compiler/heptagon/analysis/typing.ml b/compiler/heptagon/analysis/typing.ml index ebe935f..bf8f474 100644 --- a/compiler/heptagon/analysis/typing.ml +++ b/compiler/heptagon/analysis/typing.ml @@ -1164,6 +1164,8 @@ let typing_contract cenv h contract = | Some ({ c_block = b; c_assume = e_a; c_enforce = e_g; + c_assume_loc = e_a_loc; + c_enforce_loc = e_g_loc; c_controllables = c }) -> let typed_b, defined_names, h' = typing_block cenv h b in (* check that the equations do not define other unexpected names *) @@ -1171,14 +1173,18 @@ let typing_contract cenv h contract = (* assumption *) let typed_e_a = expect cenv h' (Tid Initial.pbool) e_a in + let typed_e_a_loc = expect cenv h' (Tid Initial.pbool) e_a_loc in (* property *) let typed_e_g = expect cenv h' (Tid Initial.pbool) e_g in + let typed_e_g_loc = expect cenv h' (Tid Initial.pbool) e_g_loc in let typed_c, (c_names, h) = build cenv h c in Some { c_block = typed_b; c_assume = typed_e_a; c_enforce = typed_e_g; + c_assume_loc = typed_e_a_loc; + c_enforce_loc = typed_e_g_loc; c_controllables = typed_c }, h diff --git a/compiler/heptagon/hept_mapfold.ml b/compiler/heptagon/hept_mapfold.ml index edbeae9..7306d13 100644 --- a/compiler/heptagon/hept_mapfold.ml +++ b/compiler/heptagon/hept_mapfold.ml @@ -253,10 +253,14 @@ 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_loc, acc = exp_it funs acc c.c_assume_loc in + let c_enforce_loc, acc = exp_it funs acc c.c_enforce_loc 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_assume = c_assume; c_enforce = c_enforce; + c_assume_loc = c_assume_loc; + c_enforce_loc = c_enforce_loc; c_block = c_block; c_controllables = c_controllables }, acc diff --git a/compiler/heptagon/heptagon.ml b/compiler/heptagon/heptagon.ml index 4d003be..7e120b5 100644 --- a/compiler/heptagon/heptagon.ml +++ b/compiler/heptagon/heptagon.ml @@ -144,6 +144,8 @@ and type_dec_desc = type contract = { c_assume : exp; c_enforce : exp; + c_assume_loc : exp; + c_enforce_loc : exp; c_controllables : var_dec list; c_block : block } diff --git a/compiler/heptagon/parsing/hept_parser.mly b/compiler/heptagon/parsing/hept_parser.mly index 04528d7..78a3494 100644 --- a/compiler/heptagon/parsing/hept_parser.mly +++ b/compiler/heptagon/parsing/hept_parser.mly @@ -237,6 +237,8 @@ contract: { Some{ c_block = b; c_assume = a; c_enforce = e; + c_assume_loc = mk_constructor_exp ptrue (Loc($startpos,$endpos)); + c_enforce_loc = mk_constructor_exp ptrue (Loc($startpos,$endpos)); c_controllables = w } } ; diff --git a/compiler/heptagon/parsing/hept_parsetree.ml b/compiler/heptagon/parsing/hept_parsetree.ml index 179c249..c49af63 100644 --- a/compiler/heptagon/parsing/hept_parsetree.ml +++ b/compiler/heptagon/parsing/hept_parsetree.ml @@ -172,6 +172,8 @@ and type_desc = type contract = { c_assume : exp; c_enforce : exp; + c_assume_loc : exp; + c_enforce_loc : exp; c_controllables : var_dec list; c_block : block } diff --git a/compiler/heptagon/parsing/hept_parsetree_mapfold.ml b/compiler/heptagon/parsing/hept_parsetree_mapfold.ml index d2b7044..d8d253b 100644 --- a/compiler/heptagon/parsing/hept_parsetree_mapfold.ml +++ b/compiler/heptagon/parsing/hept_parsetree_mapfold.ml @@ -238,9 +238,15 @@ 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_loc, acc = exp_it funs acc c.c_assume_loc in + let c_enforce_loc, acc = exp_it funs acc c.c_enforce_loc in let c_block, acc = block_it funs acc c.c_block in { c with - c_assume = c_assume; c_enforce = c_enforce; c_block = c_block } + c_assume = c_assume; + c_enforce = c_enforce; + c_assume_loc = c_assume_loc; + c_enforce_loc = c_enforce_loc; + c_block = c_block } , acc diff --git a/compiler/heptagon/parsing/hept_scoping.ml b/compiler/heptagon/parsing/hept_scoping.ml index 0c81ca9..cdf96c2 100644 --- a/compiler/heptagon/parsing/hept_scoping.ml +++ b/compiler/heptagon/parsing/hept_scoping.ml @@ -425,6 +425,8 @@ let translate_contract env opt_ct = let b, env = translate_block env ct.c_block in Some { Heptagon.c_assume = translate_exp env ct.c_assume; Heptagon.c_enforce = translate_exp env ct.c_enforce; + Heptagon.c_assume_loc = translate_exp env ct.c_assume_loc; + Heptagon.c_enforce_loc = translate_exp env ct.c_enforce_loc; Heptagon.c_controllables = translate_vd_list env' ct.c_controllables; Heptagon.c_block = b }, env' @@ -548,7 +550,9 @@ let translate_signature s = let o = List.map translate_arg s.sig_outputs in let p, _ = params_of_var_decs Rename.empty s.sig_params in let c = List.map translate_constrnt s.sig_param_constraints in - let sig_node = Signature.mk_node ~extern:s.sig_external s.sig_loc i o s.sig_stateful s.sig_unsafe p in + let sig_node = + Signature.mk_node + ~extern:s.sig_external s.sig_loc i o s.sig_stateful s.sig_unsafe p in Check_signature.check_signature sig_node; safe_add s.sig_loc add_value n sig_node; mk_signature n i o s.sig_stateful p c s.sig_loc ~extern:s.sig_external diff --git a/compiler/heptagon/transformations/boolean.ml b/compiler/heptagon/transformations/boolean.ml index 3d59f59..1303b47 100644 --- a/compiler/heptagon/transformations/boolean.ml +++ b/compiler/heptagon/transformations/boolean.ml @@ -836,6 +836,8 @@ let translate_contract env contract = | None -> None, env | Some { c_assume = e_a; c_enforce = e_g; + c_assume_loc = e_a_loc; + c_enforce_loc = e_g_loc; c_controllables = cl; c_block = b } -> let cl, cl_loc, cl_eq, env = buildenv_var_dec_list env cl in @@ -844,13 +846,17 @@ let translate_contract env contract = b_equs = eqs } as b), env' = translate_block env cl_loc cl_eq b in let context, e_a = translate env' (v,eqs) e_a in + let context, e_a_loc = translate env' (v,eqs) e_a_loc in let context, e_g = translate env' context e_g in + let context, e_g_loc = translate env' context e_g_loc in let (d_list,eq_list) = context in Some { c_block = { b with b_local = d_list; b_equs = eq_list }; c_assume = e_a; c_enforce = e_g; + c_assume_loc = e_a_loc; + c_enforce_loc = e_g_loc; c_controllables = cl }, env diff --git a/compiler/heptagon/transformations/normalize.ml b/compiler/heptagon/transformations/normalize.ml index b2f8c5a..6330330 100644 --- a/compiler/heptagon/transformations/normalize.ml +++ b/compiler/heptagon/transformations/normalize.ml @@ -339,11 +339,15 @@ let contract funs context c = (* Non-void context could mean lost equations *) assert (void_context=([],[])); let context, e_a = translate ExtValue ([],[]) c.c_assume in + let context, e_a_loc = translate ExtValue context c.c_assume_loc in let context, e_e = translate ExtValue context c.c_enforce in + let context, e_e_loc = translate ExtValue context c.c_enforce_loc in let (d_list, eq_list) = context in { c with c_assume = e_a; c_enforce = e_e; + c_assume_loc = e_a_loc; + c_enforce_loc = e_e_loc; c_block = { b with b_local = d_list@b.b_local; b_equs = eq_list@b.b_equs; } diff --git a/compiler/main/hept2mls.ml b/compiler/main/hept2mls.ml index 6069354..435a1a3 100644 --- a/compiler/main/hept2mls.ml +++ b/compiler/main/hept2mls.ml @@ -180,11 +180,15 @@ let translate_contract contract = Heptagon.b_equs = eq_list }; Heptagon.c_assume = e_a; Heptagon.c_enforce = e_g; + Heptagon.c_assume_loc = e_a_loc; + Heptagon.c_enforce_loc = e_g_loc; Heptagon.c_controllables = l_c } -> Some { c_local = List.map translate_var v; c_eq = List.map translate_eq eq_list; c_assume = translate_extvalue e_a; c_enforce = translate_extvalue e_g; + c_assume_loc = translate_extvalue e_a_loc; + c_enforce_loc = translate_extvalue e_g_loc; c_controllables = List.map translate_var l_c } let node n = diff --git a/compiler/minils/analysis/clocking.ml b/compiler/minils/analysis/clocking.ml index 3783a06..9e12285 100644 --- a/compiler/minils/analysis/clocking.ml +++ b/compiler/minils/analysis/clocking.ml @@ -240,6 +240,8 @@ let typing_contract h contract = c_eq = eq_list; c_assume = e_a; c_enforce = e_g; + c_assume_loc = e_a_loc; + c_enforce_loc = e_g_loc; c_controllables = c_list } as contract) -> let h' = append_env h l_list in (* assumption *) @@ -247,6 +249,8 @@ let typing_contract h contract = let eq_list = typing_eqs h' eq_list in expect_extvalue h' Cbase e_a; expect_extvalue h' Cbase e_g; + expect_extvalue h' Cbase e_a_loc; + expect_extvalue h' Cbase e_g_loc; let h = append_env h c_list in Some { contract with c_eq = eq_list }, h diff --git a/compiler/minils/minils.ml b/compiler/minils/minils.ml index 11e057a..dc656da 100644 --- a/compiler/minils/minils.ml +++ b/compiler/minils/minils.ml @@ -20,7 +20,7 @@ open Clocks (** Warning: Whenever Minils ast is modified, minils_format_version should be incremented. *) -let minils_format_version = "2" +let minils_format_version = "3" type iterator_type = | Imap @@ -121,6 +121,8 @@ type var_dec = { type contract = { c_assume : extvalue; c_enforce : extvalue; + c_assume_loc : extvalue; + c_enforce_loc : extvalue; c_controllables : var_dec list; c_local : var_dec list; c_eq : eq list } diff --git a/compiler/minils/mls_mapfold.ml b/compiler/minils/mls_mapfold.ml index da6c5a5..9f6a85a 100644 --- a/compiler/minils/mls_mapfold.ml +++ b/compiler/minils/mls_mapfold.ml @@ -162,11 +162,18 @@ 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 = extvalue_it funs acc c.c_assume in + let c_assume_loc, acc = extvalue_it funs acc c.c_assume_loc in let c_enforce, acc = extvalue_it funs acc c.c_enforce in + let c_enforce_loc, acc = extvalue_it funs acc c.c_enforce_loc 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 - c_assume = c_assume; c_enforce = c_enforce; c_local = c_local; c_eq = c_eq } + c_assume = c_assume; + c_enforce = c_enforce; + c_assume_loc = c_assume_loc; + c_enforce_loc = c_enforce_loc; + c_local = c_local; + c_eq = c_eq } , acc