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

Make Heptagon API more uniform 

Use a block instead of variable list + equation list
for contract and node.
The new program transformations based on the 
mapfold iterator are now enabled by default.
This commit is contained in:
Cédric Pasteur 2010-07-20 09:31:29 +02:00
parent e57c663f43
commit b2c88810c5
16 changed files with 90 additions and 123 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -185,20 +185,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_local = l_list; c_eq = eq_list; c_assume = e_a;
| Some { c_block = b; c_assume = e_a;
c_enforce = e_g } ->
let teq = typing_eqs eq_list in
let teq = typing_eqs b.b_equs in
let t_contract = cseq (typing e_a) (cseq teq (typing e_g)) in
Causal.check loc t_contract;
let t_contract = clear (build l_list) t_contract in
let t_contract = clear (build b.b_local) t_contract in
t_contract
let typing_node { n_name = f; n_input = i_list; n_output = o_list;
n_contract = contract;
n_local = l_list; n_equs = eq_list; n_loc = loc } =
n_block = b; n_loc = loc } =
let _ = typing_contract loc contract in
let teq = typing_eqs eq_list in
Causal.check loc teq
ignore (typing_block b)
let program ({ p_nodes = p_node_list } as p) =
List.iter typing_node p_node_list;

13
compiler/heptagon/analysis/initialization.ml
View File

@ -338,10 +338,10 @@ let sbuild h dec =
let typing_contract h contract =
match contract with
| None -> h
| Some { c_local = l_list; c_eq = eq_list; c_assume = e_a;
| Some { c_block = b; c_assume = e_a;
c_enforce = e_g } ->
let h' = build h l_list in
typing_eqs h' eq_list;
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 *)
@ -349,14 +349,11 @@ let typing_contract h contract =
h
let typing_node { n_name = f; n_input = i_list; n_output = o_list;
n_contract = contract;
n_local = l_list; n_equs = eq_list } =
n_contract = contract; n_block = b } =
let h = sbuild Env.empty i_list in
let h = sbuild h o_list in
let h = typing_contract h contract in
let h = build h l_list in
typing_eqs h eq_list
ignore (typing_block h b)
let program ({ p_nodes = p_node_list } as p) =
List.iter typing_node p_node_list;

40
compiler/heptagon/analysis/typing.ml
View File

@ -1008,27 +1008,21 @@ let typing_contract statefull const_env h contract =
match contract with
| None -> None,h
| Some ({ c_local = l_list;
c_eq = eq;
| Some ({ c_block = b;
c_assume = e_a;
c_enforce = e_g }) ->
let typed_l_list, local_names, h' = build const_env h h l_list in
let typed_eq, defined_names =
typing_eq_list statefull const_env h' Env.empty eq in
let typed_b, defined_names, _ = typing_block statefull const_env h b in
(* check that the equations do not define other unexpected names *)
included_env defined_names Env.empty;
(* assumption *)
let typed_e_a = expect statefull const_env h' (Tid Initial.pbool) e_a in
let typed_e_a = expect statefull const_env h (Tid Initial.pbool) e_a in
(* property *)
let typed_e_g = expect statefull const_env h' (Tid Initial.pbool) e_g in
let typed_e_g = expect statefull const_env h (Tid Initial.pbool) e_g in
included_env local_names defined_names;
included_env defined_names local_names;
Some { c_local = typed_l_list;
c_eq = typed_eq;
c_assume = typed_e_a;
c_enforce = typed_e_g }, h
Some { c_block = typed_b;
c_assume = typed_e_a;
c_enforce = typed_e_g }, h
let signature statefull inputs returns params constraints =
let arg_dec_of_var_dec vd =
@ -1056,7 +1050,7 @@ let build_node_params const_env l =
let node ({ n_name = f; n_statefull = statefull;
n_input = i_list; n_output = o_list;
n_contract = contract;
n_local = l_list; n_equs = eq_list; n_loc = loc;
n_block = b; n_loc = loc;
n_params = node_params; } as n) =
try
let typed_params, const_env =
@ -1071,14 +1065,13 @@ let node ({ n_name = f; n_statefull = statefull;
let typed_contract, h =
typing_contract statefull const_env h contract in
let typed_l_list, local_names, h = build const_env h h l_list in
let typed_eq_list, defined_names =
typing_eq_list statefull const_env h Env.empty eq_list in
let typed_b, defined_names, _ = typing_block statefull const_env h b in
(* check that the defined names match exactly the outputs and locals *)
included_env defined_names output_names;
included_env output_names defined_names;
(* if not (statefull) & (List.length o_list <> 1)
then error (Etoo_many_outputs);*)
let expected_names = add local_names output_names in
included_env expected_names defined_names;
included_env defined_names expected_names;
let cl = get_size_constraint () in
let cl = solve loc cl in
@ -1087,10 +1080,9 @@ let node ({ n_name = f; n_statefull = statefull;
{ n with
n_input = typed_i_list;
n_output = typed_o_list;
n_local = typed_l_list;
n_params = typed_params;
n_contract = typed_contract;
n_equs = typed_eq_list }
n_block = typed_b }
with
| TypingError(error) -> message loc error

13
compiler/heptagon/hept_mapfold.ml
View File

@ -242,10 +242,9 @@ 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_local, acc = mapfold (var_dec_it funs) acc c.c_local in
let c_eq, acc = mapfold (eq_it funs) acc c.c_eq in
let c_block, acc = block_it funs acc c.c_block 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_block = c_block }
, acc
and param_it funs acc vd = funs.param funs acc vd
@ -257,17 +256,15 @@ and node_dec_it funs acc nd = funs.node_dec funs acc nd
and node_dec funs acc nd =
let n_input, acc = mapfold (var_dec_it funs) acc nd.n_input in
let n_output, acc = mapfold (var_dec_it funs) acc nd.n_output in
let n_local, acc = mapfold (var_dec_it funs) acc nd.n_local in
let n_params, acc = mapfold (param_it funs.global_funs) acc nd.n_params in
let n_contract, acc = optional_wacc (contract_it funs) acc nd.n_contract in
let n_equs, acc = mapfold (eq_it funs) acc nd.n_equs in
let n_block, acc = block_it funs acc nd.n_block in
{ nd with
n_input = n_input;
n_output = n_output;
n_local = n_local;
n_block = n_block;
n_params = n_params;
n_contract = n_contract;
n_equs = n_equs; }
n_contract = n_contract }
, acc

22
compiler/heptagon/hept_printer.ml
View File

@ -56,7 +56,8 @@ and print_exp ff e =
| Elast x -> fprintf ff "last "; print_ident ff x
| Econst c -> print_static_exp ff c
| Epre(None, e) -> fprintf ff "pre "; print_exp ff e
| Epre(Some c, e) -> print_static_exp ff c; fprintf ff " fby "; print_exp ff e
| Epre(Some c, e) ->
print_static_exp ff c; fprintf ff " fby "; print_exp ff e
| Efby(e1, e2) -> print_exp ff e1; fprintf ff " fby "; print_exp ff e2
| Eapp({ a_op = op; a_params = params }, e_list, r) ->
print_op ff op params e_list;
@ -283,19 +284,18 @@ let print_const_dec ff c =
print_static_exp ff c.c_value;
fprintf ff "@.@]"
let print_contract ff {c_local = l;
c_eq = eqs;
let print_contract ff {c_block = b;
c_assume = e_a;
c_enforce = e_g } =
if l <> [] then begin
if b.b_local <> [] then begin
fprintf ff "@[<v 2>contract@\n";
fprintf ff "@[<hov 4>var ";
print_list_r print_vd "" ";" "" ff l;
print_list_r print_vd "" ";" "" ff b.b_local;
fprintf ff ";@]@\n"
end;
if eqs <> [] then begin
if b.b_equs <> [] then begin
fprintf ff "@[<v 2>let @,";
print_eq_list ff eqs;
print_eq_list ff b.b_equs;
fprintf ff "@]"; fprintf ff "tel@\n"
end;
fprintf ff "assume %a@;enforce %a@;with (@[<hov>"
@ -309,7 +309,7 @@ let print_node_params ff = function
let print_node ff
{ n_name = n; n_input = ni;
n_local = nl; n_output = no; n_contract = contract; n_equs = ne;
n_block = nb; n_output = no; n_contract = contract;
n_params = params; } =
fprintf ff "@[<v 2>node ";
print_name ff n;
@ -319,13 +319,13 @@ let print_node ff
fprintf ff "@[%a@]" (print_list_r print_vd "(" ";" ")") no;
fprintf ff "@,";
optunit (print_contract ff) contract;
if nl <> [] then begin
if nb.b_local <> [] then begin
fprintf ff "@[<hov 4>var ";
print_list_r print_vd "" ";" "" ff nl;
print_list_r print_vd "" ";" "" ff nb.b_local;
fprintf ff ";@]@,"
end;
fprintf ff "@[<v 2>let @,";
print_eq_list ff ne;
print_eq_list ff nb.b_equs;
fprintf ff "@]@;"; fprintf ff "tel";fprintf ff "@.@]"
let print_open_module ff name =

11
compiler/heptagon/heptagon.ml
View File

@ -68,8 +68,8 @@ and eqdesc =
and block = {
b_local : var_dec list;
b_equs : eq list;
mutable b_defnames : ty Env.t;
mutable b_statefull : bool;
b_defnames : ty Env.t;
b_statefull : bool;
b_loc : location }
and state_handler = {
@ -102,17 +102,16 @@ and type_dec_desc = Type_abs | Type_enum of name list | Type_struct of structure
type contract = {
c_assume : exp;
c_enforce : exp;
c_local : var_dec list;
c_eq : eq list }
c_block : block }
type node_dec = {
n_name : name;
n_statefull : bool;
n_input : var_dec list;
n_output : var_dec list;
n_local : var_dec list;
n_contract : contract option;
n_equs : eq list; n_loc : location;
n_block : block;
n_loc : location;
n_params : param list;
n_params_constraints : size_constraint list }

12
compiler/heptagon/main/hept_compiler.ml
View File

@ -47,26 +47,26 @@ let compile_impl pp p =
do_silent_pass Initialization.program "Initialization check" p !init in
(* Completion of partial definitions *)
let p = do_pass Completion.program "Completion" p pp true in
let p = do_pass Completion_mapfold.program "Completion" p pp true in
let p =
let call_inline_pass = (List.length !inline > 0) || !Misc.flatten in
do_pass Inline.program "Inlining" p pp call_inline_pass in
(* Automata *)
let p = do_pass Automata.program "Automata" p pp true in
let p = do_pass Automata_mapfold.program "Automata" p pp true in
(* Present *)
let p = do_pass Present.program "Present" p pp true in
let p = do_pass Present_mapfold.program "Present" p pp true in
(* Shared variables (last) *)
let p = do_pass Last.program "Last" p pp true in
let p = do_pass Last_mapfold.program "Last" p pp true in
(* Reset *)
let p = do_pass Reset.program "Reset" p pp true in
let p = do_pass Reset_mapfold.program "Reset" p pp true in
(* Every *)
let p = do_pass Every.program "Every" p pp true in
let p = do_pass Every_mapfold.program "Every" p pp true in
(* Return the transformed AST *)
p

10
compiler/heptagon/parsing/hept_parser.mly
View File

@ -159,8 +159,7 @@ node_dec:
n_input = $5;
n_output = $9;
n_contract = $11;
n_local = $12;
n_equs = $14;
n_block = mk_block $12 $14;
n_params = $3;
n_loc = Location.current_loc () }}
;
@ -207,10 +206,9 @@ node_params:
contract:
| /* empty */ {None}
| CONTRACT loc_vars opt_equs opt_assume enforce
{Some{c_local = $2;
c_eq = $3;
c_assume = $4;
c_enforce = $5 }}
{ Some{ c_block = mk_block $2 $3;
c_assume = $4;
c_enforce = $5 } }
;
opt_equs:

6
compiler/heptagon/parsing/hept_parsetree.ml
View File

@ -115,8 +115,7 @@ and type_desc =
type contract =
{ c_assume : exp;
c_enforce : exp;
c_local : var_dec list;
c_eq : eq list;
c_block : block
}
type node_dec =
@ -124,9 +123,8 @@ type node_dec =
n_statefull : bool;
n_input : var_dec list;
n_output : var_dec list;
n_local : var_dec list;
n_contract : contract option;
n_equs : eq list;
n_block : block;
n_loc : location;
n_params : var_dec list; }

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

@ -273,25 +273,25 @@ and translate_last const_env env = function
| Last (Some e) -> Heptagon.Last (Some (expect_static_exp const_env e))
let translate_contract const_env env ct =
let b, _ = translate_block const_env env ct.c_block in
{ Heptagon.c_assume = translate_exp const_env env ct.c_assume;
Heptagon.c_enforce = translate_exp const_env env ct.c_enforce;
Heptagon.c_local = translate_vd_list const_env env ct.c_local;
Heptagon.c_eq = List.map (translate_eq const_env env) ct.c_eq }
Heptagon.c_block = b }
let param_of_var_dec const_env vd =
Signature.mk_param vd.v_name (translate_type const_env vd.v_type)
let translate_node const_env env node =
let const_env = build_id_list node.n_loc const_env node.n_params in
let env = build_vd_list env (node.n_input @ node.n_output @ node.n_local) in
let env = build_vd_list env (node.n_input @ node.n_output) in
let b, env = translate_block const_env env node.n_block in
{ Heptagon.n_name = node.n_name;
Heptagon.n_statefull = node.n_statefull;
Heptagon.n_input = translate_vd_list const_env env node.n_input;
Heptagon.n_output = translate_vd_list const_env env node.n_output;
Heptagon.n_local = translate_vd_list const_env env node.n_local;
Heptagon.n_contract = Misc.optional
(translate_contract const_env env) node.n_contract;
Heptagon.n_equs = List.map (translate_eq const_env env) node.n_equs;
Heptagon.n_block = b;
Heptagon.n_loc = node.n_loc;
Heptagon.n_params = List.map (param_of_var_dec const_env) node.n_params;
Heptagon.n_params_constraints = []; }
@ -338,7 +338,8 @@ let translate_signature s =
let translate_interface_desc const_env = function
| Iopen n -> Heptagon.Iopen n
| Itypedef tydec -> Heptagon.Itypedef (translate_typedec const_env tydec)
| Iconstdef const_dec -> Heptagon.Iconstdef (translate_const_dec const_env const_dec)
| Iconstdef const_dec ->
Heptagon.Iconstdef (translate_const_dec const_env const_dec)
| Isignature s -> Heptagon.Isignature (translate_signature s)
let translate_interface_decl const_env idecl =

9
compiler/heptagon/transformations/automata_mapfold.ml
View File

@ -157,17 +157,12 @@ let rec eq funs (v, eq_list) eq =
eq, translate_automaton v eq_list state_handlers
| _ -> eq, (v, eq::eq_list)
let node_dec funs acc n =
let n, (v, eq_list) = Hept_mapfold.node_dec funs ([],[]) n in
{ n with n_local = v @ n.n_local; n_equs = eq_list @ n.n_equs; }, acc
let block funs acc b =
let b, (v, acc_eq_list) = Hept_mapfold.block funs ([], []) b in
{ b with b_local = v @ b.b_local; b_equs = acc_eq_list@b.b_equs }, acc
{ b with b_local = v @ b.b_local; b_equs = acc_eq_list }, acc
let program p =
let funs = { Hept_mapfold.defaults
with eq = eq; block = block; node_dec = node_dec } in
with eq = eq; block = block } in
let p, _ = Hept_mapfold.program_it funs ([],[]) p in
p
{ p with p_types = !state_type_dec_list @ p.p_types }

8
compiler/heptagon/transformations/every_mapfold.ml
View File

@ -1,6 +1,6 @@
open Heptagon
open Hept_mapfold
open Reset
open Reset_mapfold
let statefull eq_list = List.exists (fun eq -> eq.eq_statefull) eq_list
@ -27,12 +27,8 @@ let edesc funs (v,acc_eq_list) ed =
| _ -> ed, (v, acc_eq_list)
let node funs _ n =
let n, (v, eq_list) = Hept_mapfold.node_dec funs ([],[]) n in
{ n with n_local = v @ n.n_local; n_equs = eq_list @ n.n_equs; }, ([],[])
let program p =
let funs = { Hept_mapfold.defaults
with edesc = edesc; block = block; node_dec = node } in
with edesc = edesc; block = block } in
let p, _ = program_it funs ([],[]) p in
p

11
compiler/heptagon/transformations/inline.ml
View File

@ -21,7 +21,8 @@ let mk_unique_node nd =
let mk_bind vd =
let id = Ident.fresh (Ident.sourcename vd.v_ident) in
(vd.v_ident, { vd with v_ident = id; }) in
let subst = List.map mk_bind (nd.n_local @ nd.n_input @ nd.n_output) in
let subst = List.map mk_bind (nd.n_block.b_local
@ nd.n_input @ nd.n_output) in
let subst_var_dec funs () vd =
({ vd with v_ident = (List.assoc vd.v_ident subst).v_ident; }, ()) in
@ -81,10 +82,10 @@ let exp funs (env, newvars, newequs) exp = match exp.e_desc with
mk_equation ~statefull:false (Eeq (Evarpat vd.v_ident, e)) in
let mk_output_exp vd = mk_exp (Evar vd.v_ident) vd.v_type in
let newvars = ni.n_input @ ni.n_local @ ni.n_output @ newvars
let newvars = ni.n_input @ ni.n_block.b_local @ ni.n_output @ newvars
and newequs =
List.map2 mk_input_equ ni.n_input argl
@ List.map add_reset ni.n_equs
@ List.map add_reset ni.n_block.b_equs
@ newequs in
(* For clocking reason we cannot create 1-tuples. *)
@ -105,7 +106,9 @@ let block funs (env, newvars, newequs) blk =
let node_dec funs (env, newvars, newequs) nd =
let nd, (env, newvars, newequs) =
Hept_mapfold.node_dec funs (env, newvars, newequs) nd in
({ nd with n_local = newvars @ nd.n_local; n_equs = newequs @ nd.n_equs; },
({ nd with n_block =
{ nd.n_block with b_local = newvars @ nd.n_block.b_local;
b_equs = newequs @ nd.n_block.b_equs } },
(env, [], []))
let program p =

15
compiler/heptagon/transformations/last_mapfold.ml
View File

@ -38,23 +38,16 @@ let block funs env b =
{ b with b_local = b.b_local @ last_v;
b_equs = eq_lastn_n_list @ b.b_equs }, env
let contract funs env contract =
let eq_lastn_n_list, env', last_v = extend_env env contract.c_local in
let contract, _ = Hept_mapfold.contract funs env contract in
{ contract with c_local = contract.c_local @ last_v;
c_eq = eq_lastn_n_list @ contract.c_eq }, env
let node_dec funs env n =
let _, env, _ = extend_env Env.empty n.n_input in
let eq_lasto_list, env, last_o = extend_env env n.n_output in
let eq_lastn_n_list, env, last_v = extend_env env n.n_local in
let n, _ = Hept_mapfold.node_dec funs env n in
{ n with n_local = n.n_local @ last_o @ last_v;
n_equs = eq_lasto_list @ eq_lastn_n_list @ n.n_equs }, env
{ n with n_block =
{ n.n_block with b_local = n.n_block.b_local @ last_o;
b_equs = eq_lasto_list @ n.n_block.b_equs } }, env
let program p =
let funs = { Hept_mapfold.defaults with
node_dec = node_dec; block = block;
contract = contract; edesc = edesc } in
node_dec = node_dec; block = block; edesc = edesc } in
let p, _ = Hept_mapfold.program_it funs Env.empty p in
p

9
compiler/heptagon/transformations/reset_mapfold.ml
View File

@ -176,13 +176,12 @@ let eq funs (res, v, acc_eq_list) equ =
let equ, (res, v, acc_eq_list) = eq funs (res, v, acc_eq_list) equ in
equ, (res, v, equ::acc_eq_list)
let node funs _ n =
let n, (_, v, eq_list) = Hept_mapfold.node_dec funs (None, [], []) n in
{ n with n_local = v @ n.n_local; n_equs = eq_list; }, (None, [], [])
let block funs _ b =
let n, (_, v, eq_list) = Hept_mapfold.block funs (None, [], []) b in
{ b with b_local = v @ b.b_local; b_equs = eq_list; }, (None, [], [])
let program p =
let funs = { Hept_mapfold.defaults with
eq = eq; node_dec = node; edesc = edesc } in
eq = eq; block = block; edesc = edesc } in
let p, _ = program_it funs (None, [], []) p in
p

10
compiler/main/hept2mls.ml
View File

@ -339,8 +339,8 @@ and translate_switch_handlers env ni (locals, l_eqs, s_eqs) e handlers =
let translate_contract env contract =
match contract with
| None -> None, env
| Some { Heptagon.c_local = v;
Heptagon.c_eq = eq_list;
| Some { Heptagon.c_block = { Heptagon.b_local = v;
Heptagon.b_equs = eq_list };
Heptagon.c_assume = e_a;
Heptagon.c_enforce = e_g} ->
let env' = Env.add v env in
@ -360,14 +360,14 @@ let translate_contract env contract =
let node
{ Heptagon.n_name = n; Heptagon.n_input = i; Heptagon.n_output = o;
Heptagon.n_contract = contract;
Heptagon.n_local = l; Heptagon.n_equs = eq_list;
Heptagon.n_block = { Heptagon.b_local = v; Heptagon.b_equs = eq_list };
Heptagon.n_loc = loc;
Heptagon.n_params = params;
Heptagon.n_params_constraints = params_constr } =
let env = Env.add o (Env.add i Env.empty) in
let contract, env = translate_contract env contract in
let env = Env.add l env in
let locals = translate_locals [] l in
let env = Env.add v env in
let locals = translate_locals [] v in
let locals, l_eqs, s_eqs =
translate_eqs env IdentSet.empty (locals, [], []) eq_list in
let l_eqs, _ = add_locals IdentSet.empty l_eqs [] s_eqs in