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

Added local assume/guarantee

Browse source 
Added local assume/guarantee in contracts.

No syntax associated to these local asume/guarantee: internal use only.
This commit is contained in:
Gwenal Delaval 2012-05-29 14:14:46 +02:00
parent 8153bc4eb5
commit bb0bc8bfe5
15 changed files with 74 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

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

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

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

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

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

4
compiler/heptagon/hept_mapfold.ml
View file

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

2
compiler/heptagon/heptagon.ml
View file

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

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

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

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

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

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

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

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

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

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

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

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

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

4
compiler/main/hept2mls.ml
View file

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

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

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

4
compiler/minils/minils.ml
View file

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

9
compiler/minils/mls_mapfold.ml
View file

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