jeltz/heptagon
1
0
Fork 0
Code Issues Pull requests Releases Activity

Added syntax for reachability and attractivity in contracts

Browse source 
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"
This commit is contained in:
Gwenaël Delaval 2015-01-06 00:18:00 +01:00
parent 177f5f9f3e
commit 3dfbeffeb6
22 changed files with 256 additions and 83 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
compiler/heptagon/analysis/causality.ml
View file

@ -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

4
compiler/heptagon/analysis/hept_clocking.ml
View file

@ -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

4
compiler/heptagon/analysis/initialization.ml
View file

@ -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;

17
compiler/heptagon/analysis/typing.ml
View file

@ -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

12
compiler/heptagon/hept_mapfold.ml
View file

@ -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;

19
compiler/heptagon/hept_printer.ml
View file

@ -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 "@[<v2>contract@\n%a@ assume %a@ enforce %a@ with (%a)@\n@]"
c_assume = e_a;
c_objectives = objs;
c_controllables = c} =
fprintf ff "@[<v2>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

11
compiler/heptagon/heptagon.ml
View file

@ -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;

2
compiler/heptagon/parsing/hept_lexer.mll
View file

@ -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;

24
compiler/heptagon/parsing/hept_parser.mly
View file

@ -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:

14
compiler/heptagon/parsing/hept_parsetree.ml
View file

@ -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 }

11
compiler/heptagon/parsing/hept_parsetree_mapfold.ml
View file

@ -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;

13
compiler/heptagon/parsing/hept_scoping.ml
View file

@ -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;

16
compiler/heptagon/transformations/boolean.ml
View file

@ -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 },

43
compiler/heptagon/transformations/contracts.ml
View file

@ -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 = [];

9
compiler/heptagon/transformations/normalize.ml
View file

@ -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

14
compiler/main/hept2mls.ml
View file

@ -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 ;

4
compiler/minils/analysis/clocking.ml
View file

@ -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

35
compiler/minils/ctrln/ctrlNbacGen.ml
View file

@ -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';

18
compiler/minils/minils.ml
View file

@ -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;

10
compiler/minils/mls_mapfold.ml
View file

@ -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;

19
compiler/minils/mls_printer.ml
View file

@ -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 "@[<v2>contract@\n%a%a@ assume %a@ enforce %a@ with %a@\n@]"
c_assume = e_a;
c_objectives = objs;
c_controllables = c;} =
fprintf ff "@[<v2>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

29
compiler/minils/sigali/sigalimain.ml
View file

@ -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 *)