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

Handling of contracts in Mls2obc

Browse source 
Handling of contracts when the "z3z" target is off. Equations of contracts are
put into the node in the Mls2obc pass (done by the "z3z" code generation).
This commit is contained in:
Gwenaël Delaval 2014-02-22 23:53:49 +01:00
parent 8650ac5695
commit 478e621ac5
1 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
compiler/main/mls2obc.ml
View file

@ -697,7 +697,7 @@ let remove m d_list =
let translate_contract map mem_var_tys = let translate_contract map mem_var_tys =
function function
| None -> ([], [], [], []) | None -> ([], [], [], [], [])
| Some | Some
{ {
Minils.c_eq = eq_list; Minils.c_eq = eq_list;
@ -705,9 +705,9 @@ let translate_contract map mem_var_tys =
} -> } ->
let (v, si, j, s_list) = translate_eq_list map empty_call_context eq_list in let (v, si, j, s_list) = translate_eq_list map empty_call_context eq_list in
let d_list = translate_var_dec (v @ d_list) in let d_list = translate_var_dec (v @ d_list) in
let d_list = List.filter let m, d_list = List.partition
(fun vd -> not (List.exists (fun (i,_) -> i = vd.v_ident) mem_var_tys)) d_list in (fun vd -> List.exists (fun (i,_) -> i = vd.v_ident) mem_var_tys) d_list in
(si, j, s_list, d_list) (m, si, j, s_list, d_list)
(** Returns a map, mapping variables names to the variables (** Returns a map, mapping variables names to the variables
where they will be stored. *) where they will be stored. *)
@ -734,7 +734,7 @@ let translate_node
| Some c -> c.Minils.c_controllables, c.Minils.c_local in | Some c -> c.Minils.c_controllables, c.Minils.c_local in
let subst_map = subst_map i_list o_list c_list c_locals d_list mem_var_tys in let subst_map = subst_map i_list o_list c_list c_locals d_list mem_var_tys in
let (v, si, j, s_list) = translate_eq_list subst_map empty_call_context eq_list in let (v, si, j, s_list) = translate_eq_list subst_map empty_call_context eq_list in
let (si', j', s_list', d_list') = translate_contract subst_map mem_var_tys contract in let (m_c, si', j', s_list', d_list') = translate_contract subst_map mem_var_tys contract in
let i_list = translate_var_dec i_list in let i_list = translate_var_dec i_list in
let o_list = translate_var_dec o_list in let o_list = translate_var_dec o_list in
let d_list = translate_var_dec (v @ d_list) in let d_list = translate_var_dec (v @ d_list) in
@ -751,7 +751,7 @@ let translate_node
in in
let resetm = { m_name = Mreset; m_inputs = []; m_outputs = []; m_body = mk_block si } in let resetm = { m_name = Mreset; m_inputs = []; m_outputs = []; m_body = mk_block si } in
if stateful if stateful
then { cd_name = f; cd_stateful = true; cd_mems = m' @ m; cd_params = params; then { cd_name = f; cd_stateful = true; cd_mems = m' @ m @ m_c; cd_params = params;
cd_objs = j; cd_methods = [stepm; resetm]; cd_loc = loc; cd_mem_alloc = mem_alloc } cd_objs = j; cd_methods = [stepm; resetm]; cd_loc = loc; cd_mem_alloc = mem_alloc }
else ( else (
(* Functions won't have [Mreset] or memories, (* Functions won't have [Mreset] or memories,