From 3dfbeffeb6f1cbf33d30fcef9ad9c22b5fd4a5a0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Gwena=C3=ABl=20Delaval?= Date: Tue, 6 Jan 2015 00:18:00 +0100 Subject: [PATCH] Added syntax for reachability and attractivity in contracts Contracts can now comprise a list of objectives (in any order). One objective can be (e being a Boolean heptagon expression) : - invariance, with the syntax "enforce e" - reachability, "reachable e" - attractivity, "attractive e" --- compiler/heptagon/analysis/causality.ml | 11 ++--- compiler/heptagon/analysis/hept_clocking.ml | 4 +- compiler/heptagon/analysis/initialization.ml | 4 +- compiler/heptagon/analysis/typing.ml | 17 ++++++-- compiler/heptagon/hept_mapfold.ml | 12 +++++- compiler/heptagon/hept_printer.ml | 19 ++++++-- compiler/heptagon/heptagon.ml | 11 ++++- compiler/heptagon/parsing/hept_lexer.mll | 2 + compiler/heptagon/parsing/hept_parser.mly | 24 ++++++++--- compiler/heptagon/parsing/hept_parsetree.ml | 14 +++++- .../parsing/hept_parsetree_mapfold.ml | 11 ++++- compiler/heptagon/parsing/hept_scoping.ml | 13 +++++- compiler/heptagon/transformations/boolean.ml | 16 +++++-- .../heptagon/transformations/contracts.ml | 43 ++++++++++++------- .../heptagon/transformations/normalize.ml | 9 +++- compiler/main/hept2mls.ml | 14 ++++-- compiler/minils/analysis/clocking.ml | 4 +- compiler/minils/ctrln/ctrlNbacGen.ml | 35 +++++++++++---- compiler/minils/minils.ml | 18 +++++--- compiler/minils/mls_mapfold.ml | 10 ++++- compiler/minils/mls_printer.ml | 19 ++++++-- compiler/minils/sigali/sigalimain.ml | 29 +++++++++---- 22 files changed, 256 insertions(+), 83 deletions(-) diff --git a/compiler/heptagon/analysis/causality.ml b/compiler/heptagon/analysis/causality.ml index 62fc555..b6e0845 100644 --- a/compiler/heptagon/analysis/causality.ml +++ b/compiler/heptagon/analysis/causality.ml @@ -236,7 +236,7 @@ let typing_contract loc contract = | Some { c_block = b; c_assume = e_a; c_assume_loc = e_a_loc; - c_enforce = e_g; + c_objectives = objs; c_enforce_loc = e_g_loc; } -> let teq = typing_eqs b.b_equs in @@ -244,10 +244,11 @@ let typing_contract loc contract = cseq teq (ctuplelist - [(typing e_a); - (typing e_g); - (typing e_a_loc); - (typing e_g_loc)]) in + ((typing e_a) :: + (typing e_a_loc) :: + (typing e_g_loc) :: + (List.map (fun o -> typing o.o_exp) objs) + )) 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 6f7d0cb..db103a9 100644 --- a/compiler/heptagon/analysis/hept_clocking.ml +++ b/compiler/heptagon/analysis/hept_clocking.ml @@ -263,13 +263,13 @@ let typing_contract h contract = | None -> h | Some { c_block = b; c_assume = e_a; - c_enforce = e_g; + c_objectives = objs; c_controllables = c_list } -> let h' = typing_block h b in (* assumption *) expect h' (Etuplepat []) (Ck Clocks.Cbase) e_a; (* property *) - expect h' (Etuplepat []) (Ck Clocks.Cbase) e_g; + List.iter (fun o -> expect h' (Etuplepat []) (Ck Clocks.Cbase) o.o_exp) objs; append_env h c_list diff --git a/compiler/heptagon/analysis/initialization.ml b/compiler/heptagon/analysis/initialization.ml index 79d2937..31ea9ed 100644 --- a/compiler/heptagon/analysis/initialization.ml +++ b/compiler/heptagon/analysis/initialization.ml @@ -387,14 +387,14 @@ let typing_contract h contract = | None -> h | Some { c_block = b; c_assume = e_a; - c_enforce = e_g; + c_objectives = objs; 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); + List.iter (fun o -> expect h' o.o_exp (skeleton izero o.o_exp.e_ty)) objs; build_initialized h c let typing_node { n_input = i_list; n_output = o_list; diff --git a/compiler/heptagon/analysis/typing.ml b/compiler/heptagon/analysis/typing.ml index 42e2646..78c2e7c 100644 --- a/compiler/heptagon/analysis/typing.ml +++ b/compiler/heptagon/analysis/typing.ml @@ -1172,12 +1172,16 @@ and build cenv h dec = in mapfold var_dec (Env.empty, h) dec +let typing_objective cenv h obj = + let typed_e = expect cenv h (Tid Initial.pbool) obj.o_exp in + { obj with o_exp = typed_e } + let typing_contract cenv h contract = match contract with | None -> None,h | Some ({ c_block = b; c_assume = e_a; - c_enforce = e_g; + c_objectives = objs; c_assume_loc = e_a_loc; c_enforce_loc = e_g_loc; c_controllables = c }) -> @@ -1188,15 +1192,20 @@ 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 + (* objectives *) + let typed_objs = + List.map + (fun o -> + let typed_exp = expect cenv h' (Tid Initial.pbool) o.o_exp in + { o with o_exp = typed_exp; }) + objs 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_objectives = typed_objs; 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 bfbe558..a90c203 100644 --- a/compiler/heptagon/hept_mapfold.ml +++ b/compiler/heptagon/hept_mapfold.ml @@ -88,6 +88,7 @@ type 'a hept_it_funs = { switch_handler : 'a hept_it_funs -> 'a -> switch_handler -> switch_handler * 'a; var_dec : 'a hept_it_funs -> 'a -> var_dec -> var_dec * 'a; last : 'a hept_it_funs -> 'a -> last -> last * 'a; + objective : 'a hept_it_funs -> 'a -> objective -> objective * 'a; contract : 'a hept_it_funs -> 'a -> contract -> contract * 'a; node_dec : 'a hept_it_funs -> 'a -> node_dec -> node_dec * 'a; const_dec : 'a hept_it_funs -> 'a -> const_dec -> const_dec * 'a; @@ -277,16 +278,21 @@ and last funs acc l = match l with Last sto, acc +and objective_it funs acc o = funs.objective funs acc o +and objective funs acc o = + let e, acc = exp_it funs acc o.o_exp in + { o with o_exp = e }, acc + 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_objectives, acc = mapfold (objective_it funs) acc c.c_objectives 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_objectives = c_objectives; c_assume_loc = c_assume_loc; c_enforce_loc = c_enforce_loc; c_block = c_block; @@ -350,6 +356,7 @@ let defaults = { switch_handler = switch_handler; var_dec = var_dec; last = last; + objective = objective; contract = contract; node_dec = node_dec; const_dec = const_dec; @@ -374,6 +381,7 @@ let defaults_stop = { switch_handler = stop; var_dec = stop; last = stop; + objective = stop; contract = stop; node_dec = stop; const_dec = stop; diff --git a/compiler/heptagon/hept_printer.ml b/compiler/heptagon/hept_printer.ml index 5d40a75..74d35c4 100644 --- a/compiler/heptagon/hept_printer.ml +++ b/compiler/heptagon/hept_printer.ml @@ -338,13 +338,24 @@ let print_type_def ff { t_name = name; t_desc = tdesc } = fprintf ff " =@ %a" (print_record print_field) f_ty_list in fprintf ff "@[<2>type %a%a@]@." print_qualname name print_type_desc tdesc +let print_objective_kind ff = function + | Obj_enforce -> fprintf ff "enforce" + | Obj_reachable -> fprintf ff "reachable" + | Obj_attractive -> fprintf ff "attractive" + +let print_objective ff o = + fprintf ff "@[<2>%a@ %a]" + print_objective_kind o.o_kind + print_exp o.o_exp + let print_contract ff { c_block = b; - c_assume = e_a; c_enforce = e_g; - c_controllables = c} = - fprintf ff "@[contract@\n%a@ assume %a@ enforce %a@ with (%a)@\n@]" + c_assume = e_a; + c_objectives = objs; + c_controllables = c} = + fprintf ff "@[contract@\n%a@ assume %a%a@ with (%a)@\n@]" (print_block " do ") b print_exp e_a - print_exp e_g + (print_list print_objective "@ " "@ " "") objs print_vd_tuple c let print_node ff diff --git a/compiler/heptagon/heptagon.ml b/compiler/heptagon/heptagon.ml index 3f936d2..4a1332e 100644 --- a/compiler/heptagon/heptagon.ml +++ b/compiler/heptagon/heptagon.ml @@ -158,9 +158,18 @@ and type_dec_desc = | Type_enum of constructor_name list | Type_struct of structure +type objective_kind = + | Obj_enforce + | Obj_reachable + | Obj_attractive + +type objective = + { o_kind : objective_kind; + o_exp : exp } + type contract = { c_assume : exp; - c_enforce : exp; + c_objectives : objective list; c_assume_loc : exp; c_enforce_loc : exp; c_controllables : var_dec list; diff --git a/compiler/heptagon/parsing/hept_lexer.mll b/compiler/heptagon/parsing/hept_lexer.mll index 24ec5be..a7bbd61 100644 --- a/compiler/heptagon/parsing/hept_lexer.mll +++ b/compiler/heptagon/parsing/hept_lexer.mll @@ -79,6 +79,8 @@ List.iter (fun (str,tok) -> Hashtbl.add keyword_table str tok) [ "contract", CONTRACT; "assume", ASSUME; "enforce", ENFORCE; + "reachable", REACHABLE; + "attractive", ATTRACTIVE; "with", WITH; "inlined",INLINED; "when", WHEN; diff --git a/compiler/heptagon/parsing/hept_parser.mly b/compiler/heptagon/parsing/hept_parser.mly index dde9b81..168979f 100644 --- a/compiler/heptagon/parsing/hept_parser.mly +++ b/compiler/heptagon/parsing/hept_parser.mly @@ -66,6 +66,8 @@ open Hept_parsetree %token CONTRACT %token ASSUME %token ENFORCE +%token REACHABLE +%token ATTRACTIVE %token WITH %token WHEN WHENOT MERGE ON ONOT %token INLINED @@ -261,13 +263,13 @@ node_params: contract: | /* empty */ {None} - | CONTRACT b=opt_block a=opt_assume e=opt_enforce w=opt_with + | CONTRACT b=opt_block a=opt_assume ol=objectives w=opt_with { Some{ c_block = b; c_assume = a; - c_enforce = e; + c_objectives = ol; c_assume_loc = mk_constructor_exp ptrue (Loc($startpos,$endpos)); c_enforce_loc = mk_constructor_exp ptrue (Loc($startpos,$endpos)); - c_controllables = w } } + c_controllables = w } } ; opt_block: @@ -280,9 +282,19 @@ opt_assume: | ASSUME exp { $2 } ; -opt_enforce: - | /* empty */ { mk_constructor_exp ptrue (Loc($startpos,$endpos)) } - | ENFORCE exp { $2 } +objectives: + | /* empty */ { [] } + | o=objective ol=objectives { o :: ol } +; + +objective: + | objective_kind exp { mk_objective $1 $2 } +; + +objective_kind: + | ENFORCE { Obj_enforce } + | REACHABLE { Obj_reachable } + | ATTRACTIVE { Obj_attractive } ; opt_with: diff --git a/compiler/heptagon/parsing/hept_parsetree.ml b/compiler/heptagon/parsing/hept_parsetree.ml index 701f4ab..39a66ff 100644 --- a/compiler/heptagon/parsing/hept_parsetree.ml +++ b/compiler/heptagon/parsing/hept_parsetree.ml @@ -188,9 +188,18 @@ and type_desc = | Type_enum of dec_name list | Type_struct of (dec_name * ty) list +type objective_kind = + | Obj_enforce + | Obj_reachable + | Obj_attractive + +type objective = + { o_kind : objective_kind; + o_exp : exp } + type contract = { c_assume : exp; - c_enforce : exp; + c_objectives : objective list; c_assume_loc : exp; c_enforce_loc : exp; c_controllables : var_dec list; @@ -293,6 +302,9 @@ let mk_block locals eqs loc = { b_local = locals; b_equs = eqs; b_loc = loc; } +let mk_objective kind exp = + { o_kind = kind; o_exp = exp } + let mk_const_dec id ty e loc = { c_name = id; c_type = ty; c_value = e; c_loc = loc } diff --git a/compiler/heptagon/parsing/hept_parsetree_mapfold.ml b/compiler/heptagon/parsing/hept_parsetree_mapfold.ml index d0fbf8a..107b3f7 100644 --- a/compiler/heptagon/parsing/hept_parsetree_mapfold.ml +++ b/compiler/heptagon/parsing/hept_parsetree_mapfold.ml @@ -52,6 +52,7 @@ type 'a hept_it_funs = { var_dec : 'a hept_it_funs -> 'a -> var_dec -> var_dec * 'a; arg : 'a hept_it_funs -> 'a -> arg -> arg * 'a; last : 'a hept_it_funs -> 'a -> last -> last * 'a; + objective : 'a hept_it_funs -> 'a -> objective -> objective * 'a; contract : 'a hept_it_funs -> 'a -> contract -> contract * 'a; node_dec : 'a hept_it_funs -> 'a -> node_dec -> node_dec * 'a; const_dec : 'a hept_it_funs -> 'a -> const_dec -> const_dec * 'a; @@ -253,17 +254,21 @@ and last funs acc l = match l with let sto, acc = optional_wacc (exp_it funs) acc sto in Last sto, acc +and objective_it funs acc o = funs.objective funs acc o +and objective funs acc o = + let e, acc = exp_it funs acc o.o_exp in + { o with o_exp = e }, acc 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_objectives, acc = mapfold (objective_it funs) acc c.c_objectives 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_objectives = c_objectives; c_assume_loc = c_assume_loc; c_enforce_loc = c_enforce_loc; c_block = c_block } @@ -382,6 +387,7 @@ let defaults = { switch_handler = switch_handler; var_dec = var_dec; last = last; + objective = objective; contract = contract; node_dec = node_dec; const_dec = const_dec; @@ -414,6 +420,7 @@ let defaults_stop = { switch_handler = Global_mapfold.stop; var_dec = Global_mapfold.stop; last = Global_mapfold.stop; + objective = Global_mapfold.stop; contract = Global_mapfold.stop; node_dec = Global_mapfold.stop; const_dec = Global_mapfold.stop; diff --git a/compiler/heptagon/parsing/hept_scoping.ml b/compiler/heptagon/parsing/hept_scoping.ml index 06cfa5e..d5f94d4 100644 --- a/compiler/heptagon/parsing/hept_scoping.ml +++ b/compiler/heptagon/parsing/hept_scoping.ml @@ -443,6 +443,17 @@ and translate_last = function | Last (None) -> Heptagon.Last None | Last (Some e) -> Heptagon.Last (Some (expect_static_exp e)) +let translate_objective_kind obj = + match obj with + | Obj_enforce -> Heptagon.Obj_enforce + | Obj_reachable -> Heptagon.Obj_reachable + | Obj_attractive -> Heptagon.Obj_attractive + +let translate_objective env obj = + { Heptagon.o_kind = translate_objective_kind obj.o_kind; + Heptagon.o_exp = translate_exp env obj.o_exp + } + let translate_contract env opt_ct = match opt_ct with | None -> None, env @@ -450,7 +461,7 @@ let translate_contract env opt_ct = let env' = Rename.append env ct.c_controllables in 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_objectives = List.map (translate_objective env) ct.c_objectives; 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; diff --git a/compiler/heptagon/transformations/boolean.ml b/compiler/heptagon/transformations/boolean.ml index dc8cd5e..a9d5e35 100644 --- a/compiler/heptagon/transformations/boolean.ml +++ b/compiler/heptagon/transformations/boolean.ml @@ -850,11 +850,21 @@ and translate_eqs env eq_list = (fun context eq -> translate_eq env context eq) ([],[]) eq_list +let translate_objectives env context objs = + let context, objs = + List.fold_left + (fun (context,ol) o -> + let context, e = translate env context o.o_exp in + context, { o with o_exp = e } :: ol) + (context, []) + objs in + context, List.rev objs + let translate_contract env contract = match contract with | None -> None, env | Some { c_assume = e_a; - c_enforce = e_g; + c_objectives = objs; c_assume_loc = e_a_loc; c_enforce_loc = e_g_loc; c_controllables = cl; @@ -866,14 +876,14 @@ let translate_contract env contract = = 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' context e_a_loc in - let context, e_g = translate env' context e_g in + let context, objs = translate_objectives env' context objs 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_objectives = objs; c_assume_loc = e_a_loc; c_enforce_loc = e_g_loc; c_controllables = cl }, diff --git a/compiler/heptagon/transformations/contracts.ml b/compiler/heptagon/transformations/contracts.ml index 6c3b114..bbbef92 100644 --- a/compiler/heptagon/transformations/contracts.ml +++ b/compiler/heptagon/transformations/contracts.ml @@ -47,6 +47,17 @@ open Linearity let fresh = Idents.gen_var "contracts" +let not_exp e = mk_exp (mk_op_app (Efun pnot) [e]) tbool ~linearity:Ltop + +let (&&&) e1 e2 = mk_exp (mk_op_app (Efun pand) [e1;e2]) tbool ~linearity:Ltop +let (|||) e1 e2 = mk_exp (mk_op_app (Efun por) [e1;e2]) tbool ~linearity:Ltop + +let (=>) e1 e2 = (not_exp e1) ||| e2 + +let var_exp v = mk_exp (Evar v) tbool ~linearity:Ltop + +let true_exp = mk_exp (Econst (mk_static_bool true)) tbool ~linearity:Ltop + let mk_unique_node nd = let mk_bind vd = let id = fresh (Idents.name vd.v_ident) in @@ -93,7 +104,7 @@ let mk_unique_node nd = let subst_contract funs subst c = let c_block, subst' = subst_contract_block funs subst c.c_block in let c_assume, subst' = exp_it funs subst' c.c_assume in - let c_enforce, _subst' = exp_it funs subst' c.c_enforce in + let c_objectives, _subst' = mapfold (objective_it funs) subst' c.c_objectives in let subst = List.fold_left (fun subst vd -> @@ -104,7 +115,7 @@ let mk_unique_node nd = let c_assume_loc = c.c_assume_loc in let c_enforce_loc = c.c_enforce_loc in { c_assume = c_assume; - c_enforce = c_enforce; + c_objectives = c_objectives; c_assume_loc = c_assume_loc; c_enforce_loc = c_enforce_loc; c_block = c_block; @@ -224,9 +235,22 @@ let exp funs (env, newvars, newequs, cont_vars, contracts) exp = (* variable declarations for assume/guarantee *) let vd_a = mk_vd_bool v_a in let vd_g = mk_vd_bool v_g in + + (* Build an expression composed of every "enforce" objective of the contract *) + let rec build_enforce o_list = + match o_list with + [] -> true_exp + | [o] -> o.o_exp + | o :: l -> o.o_exp &&& (build_enforce l) in + + (* Currently, only the enforce part is used for modularity *) + let enforce_exp = + build_enforce + (List.filter (fun o -> o.o_kind = Obj_enforce) ci.c_objectives) in + (* equations for assume/guarantee *) let eq_a = mk_equation (Eeq (Evarpat v_a, ci.c_assume)) in - let eq_g = mk_equation (Eeq (Evarpat v_g, ci.c_enforce)) in + let eq_g = mk_equation (Eeq (Evarpat v_g, enforce_exp)) in let newvars = ni.n_input @ ci.c_block.b_local @ ni.n_output @ newvars @@ -268,17 +292,6 @@ let block funs (env, newvars, newequs, cont_vars, contracts) blk = }, (env, newvars, newequs, (cont_vars @ cont_vars'), contracts')) -let not_exp e = mk_exp (mk_op_app (Efun pnot) [e]) tbool ~linearity:Ltop - -let (&&&) e1 e2 = mk_exp (mk_op_app (Efun pand) [e1;e2]) tbool ~linearity:Ltop -let (|||) e1 e2 = mk_exp (mk_op_app (Efun por) [e1;e2]) tbool ~linearity:Ltop - -let (=>) e1 e2 = (not_exp e1) ||| e2 - -let var_exp v = mk_exp (Evar v) tbool ~linearity:Ltop - -let true_exp = mk_exp (Econst (mk_static_bool true)) tbool ~linearity:Ltop - let node_dec funs (env, newvars, newequs, cont_vars, contracts) nd = let nd, (env, newvars, newequs, _cont_vars, contracts) = Hept_mapfold.node_dec funs (env, newvars, newequs, cont_vars, contracts) nd in @@ -308,7 +321,7 @@ let node_dec funs (env, newvars, newequs, cont_vars, contracts) nd = c,[] -> c | None,_::_ -> Some { c_assume = true_exp; - c_enforce = true_exp; + c_objectives = []; c_assume_loc = assume_loc; c_enforce_loc = enforce_loc; c_controllables = []; diff --git a/compiler/heptagon/transformations/normalize.ml b/compiler/heptagon/transformations/normalize.ml index 18f37f4..25c8a9c 100644 --- a/compiler/heptagon/transformations/normalize.ml +++ b/compiler/heptagon/transformations/normalize.ml @@ -370,13 +370,18 @@ 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_e = translate ExtValue context c.c_enforce in + let context, e_e = + mapfold_right + (fun o context -> + let context, e = translate ExtValue context o.o_exp in + context, { o with o_exp = e }) + c.c_objectives context in let local_context, e_a_loc = translate ExtValue ([],[]) c.c_assume_loc in let local_context, e_e_loc = translate ExtValue local_context c.c_enforce_loc in let (d_list, eq_list) = context in { c with c_assume = e_a; - c_enforce = e_e; + c_objectives = e_e; c_assume_loc = e_a_loc; c_enforce_loc = e_e_loc; c_block = { b with diff --git a/compiler/main/hept2mls.ml b/compiler/main/hept2mls.ml index d98cece..d848f53 100644 --- a/compiler/main/hept2mls.ml +++ b/compiler/main/hept2mls.ml @@ -190,20 +190,29 @@ let translate_eq { Heptagon.eq_desc = desc; Heptagon.eq_loc = loc } = | Heptagon.Epresent _ | Heptagon.Eautomaton _ | Heptagon.Ereset _ -> Error.message loc Error.Eunsupported_language_construct +let translate_objective o = + let e = translate_extvalue o.Heptagon.o_exp in + let kind = + match o.Heptagon.o_kind with + | Heptagon.Obj_enforce -> Obj_enforce + | Heptagon.Obj_reachable -> Obj_reachable + | Heptagon.Obj_attractive -> Obj_attractive in + { o_kind = kind; o_exp = e } + let translate_contract contract = match contract with | None -> None | 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_objectives = objs; 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_objectives = List.map translate_objective objs; c_assume_loc = translate_extvalue e_a_loc; c_enforce_loc = translate_extvalue e_g_loc; c_controllables = List.map translate_var l_c } @@ -216,7 +225,6 @@ let node n = n_input = List.map translate_var n.Heptagon.n_input; n_output = List.map translate_var n.Heptagon.n_output; n_contract = translate_contract n.Heptagon.n_contract; - n_controller_call = ([],[]); n_local = List.map translate_var n.Heptagon.n_block.Heptagon.b_local; n_equs = List.map translate_eq n.Heptagon.n_block.Heptagon.b_equs; n_loc = n.Heptagon.n_loc ; diff --git a/compiler/minils/analysis/clocking.ml b/compiler/minils/analysis/clocking.ml index c2bd993..1761605 100644 --- a/compiler/minils/analysis/clocking.ml +++ b/compiler/minils/analysis/clocking.ml @@ -261,7 +261,7 @@ let typing_contract h0 h contract = | Some ({ c_local = l_list; c_eq = eq_list; c_assume = e_a; - c_enforce = e_g; + c_objectives = objs; c_assume_loc = e_a_loc; c_enforce_loc = e_g_loc; c_controllables = c_list } as contract) -> @@ -270,7 +270,7 @@ let typing_contract h0 h contract = (* property *) let eq_list = typing_eqs h' eq_list in expect_extvalue h' Clocks.Cbase e_a; - expect_extvalue h' Clocks.Cbase e_g; + List.iter (fun o -> expect_extvalue h' Clocks.Cbase o.o_exp) objs; expect_extvalue h Clocks.Cbase e_a_loc; expect_extvalue h Clocks.Cbase e_g_loc; let h = append_env h c_list in diff --git a/compiler/minils/ctrln/ctrlNbacGen.ml b/compiler/minils/ctrln/ctrlNbacGen.ml index ba7b00d..f98d1d1 100644 --- a/compiler/minils/ctrln/ctrlNbacGen.ml +++ b/compiler/minils/ctrln/ctrlNbacGen.ml @@ -68,7 +68,8 @@ type 'f gen_data = init_state: 'f bexp; assertion: 'f bexp; invariant: 'f bexp; - (* reachable: bexp; *) + reachable: 'f bexp option; + attractive: 'f bexp option; remaining_contrs: SSet.t; (* All controllable inputs that has not yet been assigned to a U/C group. *) local_contr_deps: SSet.t SMap.t; (* All variables that depend on a @@ -95,6 +96,8 @@ let mk_gen_data typdefs decls input local output init_cond = init_state = tt; assertion = tt; invariant = tt; + reachable = None; + attractive = None; } (* --- *) @@ -388,7 +391,7 @@ let declare_contrs acc cl = (** Contract translation *) let translate_contract ~pref gd ({ c_local; c_eq = equs; - c_assume = a; c_enforce = g; + c_assume = a; c_objectives = objs; c_assume_loc = a'; c_enforce_loc = g'; c_controllables = cl } as contract) = @@ -398,7 +401,7 @@ let translate_contract ~pref gd let gd = { gd with decls; contrs; remaining_contrs = c; } in let gd, equs' = translate_eqs ~pref (gd, []) equs in let ak = as_bexp & mk_and (translate_ext ~pref a) (translate_ext ~pref a') - and ok = as_bexp & mk_and (translate_ext ~pref g) (translate_ext ~pref g') in + and ok = as_bexp & translate_ext ~pref g' in let gd, ok, locals = (* Generate error variable if needed: *) if !Compiler_options.nosink @@ -410,9 +413,25 @@ let translate_contract ~pref gd mk_var_dec sink Initial.tbool Linearity.Ltop Clocks.Cbase :: locals) in - let assertion = mk_and' gd.assertion ak - and invariant = mk_and' gd.invariant ok in - ({ gd with assertion; invariant; }, { contract with c_eq = equs'; }, locals) + let gd = { gd with + assertion = mk_and' gd.assertion ak; + invariant = mk_and' gd.invariant ok; } in + + let opt_and opt_e e' = + match opt_e with + None -> Some e' + | Some e -> Some (mk_and' e e') in + + let add_objective gd o = + let e = as_bexp & translate_ext ~pref o.o_exp in + match o.o_kind with + | Obj_enforce -> { gd with invariant = mk_and' gd.invariant e; } + | Obj_reachable -> { gd with reachable = opt_and gd.reachable e; } + | Obj_attractive -> { gd with attractive = opt_and gd.attractive e; } in + + let gd = List.fold_left add_objective gd objs in + + (gd, { contract with c_eq = equs'; }, locals) (* --- *) @@ -560,8 +579,8 @@ let translate_node ~requal_types typdefs = function cn_init = mk_and' gd.init_state init_cond; cn_assertion = (* mk_or' init_cond *)gd.assertion; cn_invariant = Some (mk_or' init_cond gd.invariant); - cn_reachable = None; - cn_attractive = None; } + cn_reachable = gd.reachable; + cn_attractive = gd.attractive; } and node = { node with n_equs = equs'; diff --git a/compiler/minils/minils.ml b/compiler/minils/minils.ml index 93d9c37..2e34c73 100644 --- a/compiler/minils/minils.ml +++ b/compiler/minils/minils.ml @@ -39,7 +39,7 @@ open Clocks (** Warning: Whenever Minils ast is modified, minils_format_version should be incremented. *) -let minils_format_version = "3" +let minils_format_version = "4" type iterator_type = | Imap @@ -137,9 +137,18 @@ type var_dec = { v_clock : Clocks.ck; v_loc : location } +type objective_kind = + | Obj_enforce + | Obj_reachable + | Obj_attractive + +type objective = + { o_kind : objective_kind; + o_exp : extvalue } + type contract = { c_assume : extvalue; - c_enforce : extvalue; + c_objectives : objective list; c_assume_loc : extvalue; c_enforce_loc : extvalue; c_controllables : var_dec list; @@ -153,8 +162,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 : string list * string list; n_local : var_dec list; n_equs : eq list; n_loc : location; @@ -235,7 +242,7 @@ let mk_equation ?(loc = no_location) ?(base_ck=fresh_clock()) unsafe pat exp = { eq_lhs = pat; eq_rhs = exp; eq_unsafe = unsafe; eq_base_ck = base_ck; eq_loc = loc } let mk_node - ?(input = []) ?(output = []) ?(contract = None) ?(pinst = ([],[])) + ?(input = []) ?(output = []) ?(contract = None) ?(local = []) ?(eq = []) ?(stateful = true) ~unsafe ?(loc = no_location) ?(param = []) ?(constraints = []) ?(mem_alloc=[]) @@ -246,7 +253,6 @@ let mk_node n_input = input; n_output = output; n_contract = contract; - n_controller_call = pinst; n_local = local; n_equs = eq; n_loc = loc; diff --git a/compiler/minils/mls_mapfold.ml b/compiler/minils/mls_mapfold.ml index 24f2845..e33307c 100644 --- a/compiler/minils/mls_mapfold.ml +++ b/compiler/minils/mls_mapfold.ml @@ -47,6 +47,7 @@ type 'a mls_it_funs = { pat: 'a mls_it_funs -> 'a -> Minils.pat -> Minils.pat * 'a; var_dec: 'a mls_it_funs -> 'a -> Minils.var_dec -> Minils.var_dec * 'a; var_decs: 'a mls_it_funs -> 'a -> Minils.var_dec list -> Minils.var_dec list * 'a; + objective: 'a mls_it_funs -> 'a -> Minils.objective -> Minils.objective * 'a; contract: 'a mls_it_funs -> 'a -> Minils.contract -> Minils.contract * 'a; node_dec: 'a mls_it_funs -> 'a -> Minils.node_dec -> Minils.node_dec * 'a; const_dec: 'a mls_it_funs -> 'a -> Minils.const_dec -> Minils.const_dec * 'a; @@ -178,18 +179,22 @@ and var_dec funs acc vd = and var_decs_it funs acc vds = funs.var_decs funs acc vds and var_decs funs acc vds = mapfold (var_dec_it funs) acc vds +and objective_it funs acc o = funs.objective funs acc o +and objective funs acc o = + let e, acc = extvalue_it funs acc o.o_exp in + { o with o_exp = e }, acc 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_objectives, acc = mapfold (objective_it funs) acc c.c_objectives 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_objectives = c_objectives; c_assume_loc = c_assume_loc; c_enforce_loc = c_enforce_loc; c_local = c_local; @@ -267,6 +272,7 @@ let defaults = { pat = pat; var_dec = var_dec; var_decs = var_decs; + objective = objective; contract = contract; node_dec = node_dec; const_dec = const_dec; diff --git a/compiler/minils/mls_printer.ml b/compiler/minils/mls_printer.ml index 06608c8..1680eda 100644 --- a/compiler/minils/mls_printer.ml +++ b/compiler/minils/mls_printer.ml @@ -231,14 +231,25 @@ let print_type_dec ff { t_name = name; t_desc = tdesc } = fprintf ff "@[<2>type %a%a@]@." print_qualname name print_type_desc tdesc +let print_objective_kind ff = function + | Obj_enforce -> fprintf ff "enforce" + | Obj_reachable -> fprintf ff "reachable" + | Obj_attractive -> fprintf ff "attractive" + +let print_objective ff o = + fprintf ff "@[<2>%a@ %a]" + print_objective_kind o.o_kind + print_extvalue o.o_exp + let print_contract ff { c_local = l; c_eq = eqs; - c_assume = e_a; c_enforce = e_g; - c_controllables = c;} = - fprintf ff "@[contract@\n%a%a@ assume %a@ enforce %a@ with %a@\n@]" + c_assume = e_a; + c_objectives = objs; + c_controllables = c;} = + fprintf ff "@[contract@\n%a%a@ assume %a%a@ with %a@\n@]" print_local_vars l print_eqs eqs print_extvalue e_a - print_extvalue e_g + (print_list print_objective "@ " "@ " "") objs print_vd_tuple c diff --git a/compiler/minils/sigali/sigalimain.ml b/compiler/minils/sigali/sigalimain.ml index 12d1e82..8fc2f91 100644 --- a/compiler/minils/sigali/sigalimain.ml +++ b/compiler/minils/sigali/sigalimain.ml @@ -346,28 +346,41 @@ let translate_contract f contract = let body = [{ stmt_name = var_g; stmt_def = Sconst(Ctrue) }; { stmt_name = var_a; stmt_def = Sconst(Ctrue) }] in - [],[],[],body,(Sigali.Svar(var_a),Sigali.Svar(var_g)),[],[],[] + [],[],[],body,(Sigali.Svar(var_a),Sigali.Svar(var_g)),[],[],[],[] | Some {Minils.c_local = locals; Minils.c_eq = l_eqs; Minils.c_assume = e_a; - Minils.c_enforce = e_g; + Minils.c_objectives = objs; Minils.c_assume_loc = e_a_loc; Minils.c_enforce_loc = e_g_loc; Minils.c_controllables = cl} -> let states,init,inputs,body = translate_eq_list f l_eqs in let e_a = translate_ext prefix e_a in - let e_g = translate_ext prefix e_g in let e_a_loc = translate_ext prefix e_a_loc in let e_g_loc = translate_ext prefix e_g_loc in + + (* separate reachability and attractivity and build one security objective [e_g] *) + let e_g,sig_objs = + List.fold_left + (fun (e_g,sig_objs) o -> + let e_obj = translate_ext prefix o.Minils.o_exp in + match o.Minils.o_kind with + | Minils.Obj_enforce -> (e_g &~ e_obj), sig_objs + | Minils.Obj_reachable -> e_g, (Reachability e_obj) :: sig_objs + | Minils.Obj_attractive -> e_g, (Attractivity e_obj) :: sig_objs) + (e_g_loc,[]) + objs in + let sig_objs = List.rev sig_objs in + let body = - {stmt_name = var_g; stmt_def = e_g &~ e_g_loc } :: + {stmt_name = var_g; stmt_def = e_g } :: {stmt_name = var_a; stmt_def = e_a &~ e_a_loc } :: body in let controllables = List.map (fun ({ Minils.v_ident = id } as v) -> v,(prefix ^ (name id))) cl in states,init,inputs,body,(Sigali.Svar(var_a),Sigali.Svar(var_g)), - controllables,(locals@cl),l_eqs + controllables,(locals@cl),l_eqs,sig_objs @@ -395,7 +408,7 @@ let translate_node (fun { Minils.v_ident = v } -> f ^ "_" ^ (name v)) o_list in let states,init,add_inputs,body = translate_eq_list f eq_list in - let states_c,init_c,inputs_c,body_c,(a_c,g_c),controllables,locals_c,eqs_c = + let states_c,init_c,inputs_c,body_c,(a_c,g_c),controllables,locals_c,eqs_c,objs = translate_contract f contract in let inputs = inputs @ add_inputs @ inputs_c in let body = List.rev body in @@ -429,7 +442,7 @@ let translate_node (Slist[g_c]))] in (body_sink, sig_states_full, Sigali.Svar(error_state_name)) end in - let obj = Security(obj_exp) in + let objs = Security(obj_exp) :: objs in let p = { proc_dep = []; proc_name = f; proc_inputs = sig_inputs@sig_ctrl; @@ -440,7 +453,7 @@ let translate_node proc_init = init@init_c; proc_constraints = constraints; proc_body = body@body_c@body_sink; - proc_objectives = [obj] } in + proc_objectives = objs } in if !Compiler_options.nbvars then begin (* Print out nb of vars *)