Revision 03c767b1
Added by Pierre-Loïc Garoche almost 4 years ago
| src/tools/seal/seal_export.ml | ||
|---|---|---|
| 5 | 5 |
*) |
| 6 | 6 |
open Lustre_types |
| 7 | 7 |
open Machine_code_types |
| 8 |
open Seal_utils |
|
| 8 | 9 |
|
| 9 | 10 |
let verbose = true |
| 10 |
|
|
| 11 |
let sw_to_lustre m sw_init sw_step init_out update_out = |
|
| 12 |
let orig_nd = m.mname in |
|
| 13 |
let copy_nd = orig_nd (*Corelang.copy_node orig_nd *) in |
|
| 14 |
let vl = (* memories *) |
|
| 15 |
match sw_init with |
|
| 16 |
| [] -> assert false |
|
| 17 |
| (gl, up)::_ -> List.map (fun (v,_) -> v) up |
|
| 18 |
in |
|
| 19 |
(* let add_pre sw = |
|
| 20 |
List.map (fun (gl, up) -> |
|
| 21 |
List.map (fun (g,b) -> |
|
| 22 |
if not b then |
|
| 23 |
assert false (* should be guaranted by constrauction *) |
|
| 24 |
else |
|
| 25 |
add_pre_expr vl g) gl, |
|
| 26 |
List.map (fun (v,e) -> add_pre_expr vl e) up |
|
| 27 |
) sw |
|
| 28 |
in |
|
| 29 |
*) |
|
| 30 |
|
|
| 31 |
let process_sw vars f_e sw = |
|
| 32 |
let process_branch g_opt up = |
|
| 33 |
let el = List.map (fun (v,e) -> v, f_e e) up in |
|
| 34 |
(* Sorting list of elements, according to vars, safety check to |
|
| 11 |
|
|
| 12 |
let process_sw vars f_e sw = |
|
| 13 |
let process_branch g_opt up = |
|
| 14 |
let el = List.map (fun (v,e) -> v, f_e e) up in |
|
| 15 |
(* Sorting list of elements, according to vars, safety check to |
|
| 35 | 16 |
ensure that no variable is forgotten. *) |
| 36 |
let el, forgotten = List.fold_right (fun v (res, remaining) -> |
|
| 37 |
let vid = v.var_id in |
|
| 38 |
if List.mem_assoc vid remaining then |
|
| 39 |
((List.assoc vid remaining)::res), |
|
| 40 |
(List.remove_assoc vid remaining) |
|
| 41 |
else |
|
| 42 |
assert false (* Missing variable v in list *) |
|
| 43 |
) vars ([], el) |
|
| 44 |
in |
|
| 45 |
assert (forgotten = []); |
|
| 46 |
let loc = (List.hd el).expr_loc in |
|
| 47 |
let new_e = Corelang.mkexpr loc (Expr_tuple el) in |
|
| 48 |
match g_opt with |
|
| 49 |
None -> None, new_e, loc |
|
| 50 |
| Some g -> |
|
| 51 |
let g = f_e g in |
|
| 52 |
let ee = Corelang.mkeexpr loc g in |
|
| 53 |
let new_e = if verbose then |
|
| 54 |
{new_e with
|
|
| 55 |
expr_annot = |
|
| 56 |
Some ({annots = [["seal";"guards"],ee];
|
|
| 57 |
annot_loc = loc})} else new_e |
|
| 58 |
in |
|
| 59 |
Some g, new_e, loc |
|
| 17 |
let el, forgotten = List.fold_right (fun v (res, remaining) -> |
|
| 18 |
let vid = v.var_id in |
|
| 19 |
if List.mem_assoc vid remaining then |
|
| 20 |
((List.assoc vid remaining)::res), |
|
| 21 |
(List.remove_assoc vid remaining) |
|
| 22 |
else ( |
|
| 23 |
Format.eprintf |
|
| 24 |
"Looking for variable %s in remaining expressions: [%a]@." |
|
| 25 |
vid |
|
| 26 |
(Utils.fprintf_list ~sep:";@ " |
|
| 27 |
(fun fmt (id,e) -> |
|
| 28 |
Format.fprintf fmt |
|
| 29 |
"(%s -> %a)" |
|
| 30 |
id |
|
| 31 |
Printers.pp_expr e)) |
|
| 32 |
remaining; |
|
| 33 |
assert false (* Missing variable v in list *) |
|
| 34 |
) |
|
| 35 |
) vars ([], el) |
|
| 60 | 36 |
in |
| 61 |
let rec process_sw f_e sw = |
|
| 62 |
match sw with |
|
| 37 |
assert (forgotten = []); |
|
| 38 |
let loc = (List.hd el).expr_loc in |
|
| 39 |
let new_e = Corelang.mkexpr loc (Expr_tuple el) in |
|
| 40 |
match g_opt with |
|
| 41 |
None -> None, new_e, loc |
|
| 42 |
| Some g -> |
|
| 43 |
let g = f_e g in |
|
| 44 |
let ee = Corelang.mkeexpr loc g in |
|
| 45 |
let new_e = if verbose then |
|
| 46 |
{new_e with
|
|
| 47 |
expr_annot = |
|
| 48 |
Some ({annots = [["seal";"guards"],ee];
|
|
| 49 |
annot_loc = loc})} else new_e |
|
| 50 |
in |
|
| 51 |
Some g, new_e, loc |
|
| 52 |
in |
|
| 53 |
let rec process_sw f_e sw = |
|
| 54 |
match sw with |
|
| 63 | 55 |
| [] -> assert false |
| 64 | 56 |
| [g_opt,up] -> ((* last case, no need to guard it *) |
| 65 | 57 |
let _, up_e, _ = process_branch g_opt up in |
| ... | ... | |
| 68 | 60 |
| (g_opt,up)::tl -> |
| 69 | 61 |
let g_opt, up_e, loc = process_branch g_opt up in |
| 70 | 62 |
match g_opt with |
| 71 |
| None -> assert false (* How could this happen anyway ? *) |
|
| 63 |
| None -> ( |
|
| 64 |
Format.eprintf "SEAL issue: process_sw with %a" |
|
| 65 |
pp_sys sw |
|
| 66 |
; |
|
| 67 |
assert false (* How could this happen anyway ? *) |
|
| 68 |
) |
|
| 72 | 69 |
| Some g -> |
| 73 | 70 |
let tl_e = process_sw f_e tl in |
| 74 | 71 |
Corelang.mkexpr loc (Expr_ite (g, up_e, tl_e)) |
| 75 |
in |
|
| 76 |
process_sw f_e sw |
|
| 77 | 72 |
in |
| 73 |
process_sw f_e sw |
|
| 74 |
|
|
| 78 | 75 |
|
| 76 |
let sw_to_lustre m sw_init sw_step init_out update_out = |
|
| 77 |
let orig_nd = m.mname in |
|
| 78 |
let copy_nd = orig_nd (*Corelang.copy_node orig_nd *) in |
|
| 79 |
let vl = (* memories *) |
|
| 80 |
match sw_init with |
|
| 81 |
| [] -> assert false |
|
| 82 |
| (gl, up)::_ -> List.map (fun (v,_) -> v) up |
|
| 83 |
in |
|
| 79 | 84 |
let e_init = process_sw m.mmemory (fun x -> x) sw_init in |
| 80 | 85 |
let e_step = process_sw m.mmemory (Corelang.add_pre_expr vl) sw_step in |
| 81 | 86 |
let e_init_out = process_sw copy_nd.node_outputs (fun x -> x) init_out in |
| ... | ... | |
| 96 | 101 |
eq_rhs = Corelang.mkexpr loc (Expr_arrow(e_init_out, e_update_out)) |
| 97 | 102 |
}; |
| 98 | 103 |
]; |
| 99 |
(*node_spec = Some (Contract contract);*) |
|
| 100 |
|
|
| 101 |
(* |
|
| 102 |
il faut mettre un pre devant chaque memoire dans les updates comme dans les gardes par contre pas besoin de mettre de pre devant les entrees, ni dans les updates, ni dans les gardes |
|
| 103 |
|
|
| 104 |
|
|
| 105 |
ecrire une expression |
|
| 106 |
|
|
| 107 |
(mem1, mem2, mem3) = if garde1 then (e1,e2,e2) else if garde2 then (e1,e2,e3) else ...... else (* garde3 *) (e1,e2,e2) |
|
| 108 |
|
|
| 109 |
Il faut aussi calculer la fonction de sortie |
|
| 110 |
|
|
| 111 |
out1,out2 = if garde1 then e1,e2 else if garde2 .... |
|
| 112 |
*) |
|
| 113 | 104 |
} |
| 114 | 105 |
in |
| 115 | 106 |
new_nd, orig_nd |
Also available in: Unified diff
Seal: solved issue with guards merging