Revision ca7ff3f7
Added by Lélio Brun over 1 year ago
| src/tools/seal/seal_export.ml | ||
|---|---|---|
| 1 |
(* Multiple export channels for switched systems: |
|
| 2 |
- lustre |
|
| 3 |
- matlab |
|
| 4 |
- text |
|
| 5 |
*) |
|
| 1 |
(* Multiple export channels for switched systems: - lustre - matlab - text *) |
|
| 6 | 2 |
open Lustre_types |
| 7 | 3 |
open Machine_code_types |
| 8 | 4 |
open Seal_utils |
| ... | ... | |
| 11 | 7 |
|
| 12 | 8 |
let process_sw vars f_e sw = |
| 13 | 9 |
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 |
|
| 16 |
ensure that no variable is forgotten. *) |
|
| 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) |
|
| 10 |
let el = List.map (fun (v, e) -> v, f_e e) up in |
|
| 11 |
(* Sorting list of elements, according to vars, safety check to ensure that |
|
| 12 |
no variable is forgotten. *) |
|
| 13 |
let el, forgotten = |
|
| 14 |
List.fold_right |
|
| 15 |
(fun v (res, remaining) -> |
|
| 16 |
let vid = v.var_id in |
|
| 17 |
if List.mem_assoc vid remaining then |
|
| 18 |
List.assoc vid remaining :: res, List.remove_assoc vid remaining |
|
| 19 |
else ( |
|
| 20 |
Format.eprintf |
|
| 21 |
"Looking for variable %s in remaining expressions: [%a]@." vid |
|
| 22 |
(Utils.fprintf_list ~sep:";@ " (fun fmt (id, e) -> |
|
| 23 |
Format.fprintf fmt "(%s -> %a)" id Printers.pp_expr e)) |
|
| 24 |
remaining; |
|
| 25 |
assert false (* Missing variable v in list *))) |
|
| 26 |
vars ([], el) |
|
| 36 | 27 |
in |
| 37 | 28 |
assert (forgotten = []); |
| 38 | 29 |
let loc = (List.hd el).expr_loc in |
| 39 | 30 |
let new_e = Corelang.mkexpr loc (Expr_tuple el) in |
| 40 | 31 |
match g_opt with |
| 41 |
None -> None, new_e, loc |
|
| 32 |
| None -> |
|
| 33 |
None, new_e, loc |
|
| 42 | 34 |
| 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 |
|
| 35 |
let g = f_e g in |
|
| 36 |
let ee = Corelang.mkeexpr loc g in |
|
| 37 |
let new_e = |
|
| 38 |
if verbose then |
|
| 39 |
{
|
|
| 40 |
new_e with |
|
| 41 |
expr_annot = |
|
| 42 |
Some { annots = [ [ "seal"; "guards" ], ee ]; annot_loc = loc };
|
|
| 43 |
} |
|
| 44 |
else new_e |
|
| 45 |
in |
|
| 46 |
Some g, new_e, loc |
|
| 52 | 47 |
in |
| 53 |
let rec process_sw f_e sw =
|
|
| 48 |
let rec process_sw f_e sw = |
|
| 54 | 49 |
match sw with |
| 55 |
| [] -> assert false |
|
| 56 |
| [g_opt,up] -> ((* last case, no need to guard it *) |
|
| 50 |
| [] -> |
|
| 51 |
assert false |
|
| 52 |
| [ (g_opt, up) ] -> |
|
| 53 |
(* last case, no need to guard it *) |
|
| 57 | 54 |
let _, up_e, _ = process_branch g_opt up in |
| 58 | 55 |
up_e |
| 59 |
) |
|
| 60 |
| (g_opt,up)::tl -> |
|
| 61 |
let g_opt, up_e, loc = process_branch g_opt up in |
|
| 62 |
match g_opt with |
|
| 63 |
| None -> ( |
|
| 64 |
Format.eprintf "SEAL issue: process_sw with %a" |
|
| 65 |
(pp_sys Printers.pp_expr) sw |
|
| 66 |
; |
|
| 67 |
assert false (* How could this happen anyway ? *) |
|
| 68 |
) |
|
| 69 |
| Some g -> |
|
| 70 |
let tl_e = process_sw f_e tl in |
|
| 71 |
Corelang.mkexpr loc (Expr_ite (g, up_e, tl_e)) |
|
| 56 |
| (g_opt, up) :: tl -> ( |
|
| 57 |
let g_opt, up_e, loc = process_branch g_opt up in |
|
| 58 |
match g_opt with |
|
| 59 |
| None -> |
|
| 60 |
Format.eprintf "SEAL issue: process_sw with %a" |
|
| 61 |
(pp_sys Printers.pp_expr) sw; |
|
| 62 |
assert false (* How could this happen anyway ? *) |
|
| 63 |
| Some g -> |
|
| 64 |
let tl_e = process_sw f_e tl in |
|
| 65 |
Corelang.mkexpr loc (Expr_ite (g, up_e, tl_e))) |
|
| 72 | 66 |
in |
| 73 | 67 |
process_sw f_e sw |
| 74 | 68 |
|
| 75 |
|
|
| 76 | 69 |
let sw_to_lustre m sw_init sw_step init_out update_out = |
| 77 | 70 |
let orig_nd = m.mname in |
| 78 | 71 |
let copy_nd = orig_nd (*Corelang.copy_node orig_nd *) in |
| 79 |
let vl = (* vl are memories *) |
|
| 72 |
let vl = |
|
| 73 |
(* vl are memories *) |
|
| 80 | 74 |
match sw_init with |
| 81 |
| [] -> [] (* the system is stateless. Returning an empty list |
|
| 82 |
shall do the job *) |
|
| 83 |
|
|
| 84 |
| (_, up)::_ -> |
|
| 85 |
List.map (fun (v,_) -> v) up |
|
| 75 |
| [] -> |
|
| 76 |
[] (* the system is stateless. Returning an empty list shall do the job *) |
|
| 77 |
| (_, up) :: _ -> |
|
| 78 |
List.map (fun (v, _) -> v) up |
|
| 86 | 79 |
in |
| 87 | 80 |
let loc = Location.dummy_loc in |
| 88 | 81 |
let mem_eq = |
| 89 |
if m.mmemory = [] then |
|
| 90 |
[] |
|
| 82 |
if m.mmemory = [] then [] |
|
| 91 | 83 |
else |
| 92 | 84 |
let e_init = process_sw m.mmemory (fun x -> x) sw_init in |
| 93 | 85 |
let e_step = process_sw m.mmemory (Corelang.add_pre_expr vl) sw_step in |
| 94 |
[Eq |
|
| 95 |
{ eq_loc = loc;
|
|
| 96 |
eq_lhs = vl; |
|
| 97 |
eq_rhs = Corelang.mkexpr loc (Expr_arrow(e_init, e_step)) |
|
| 98 |
}] |
|
| 86 |
[ |
|
| 87 |
Eq |
|
| 88 |
{
|
|
| 89 |
eq_loc = loc; |
|
| 90 |
eq_lhs = vl; |
|
| 91 |
eq_rhs = Corelang.mkexpr loc (Expr_arrow (e_init, e_step)); |
|
| 92 |
}; |
|
| 93 |
] |
|
| 99 | 94 |
in |
| 100 | 95 |
let output_eq = |
| 101 | 96 |
let e_init_out = process_sw copy_nd.node_outputs (fun x -> x) init_out in |
| 102 |
let e_update_out = process_sw copy_nd.node_outputs (Corelang.add_pre_expr vl) update_out in |
|
| 103 |
[ |
|
| 97 |
let e_update_out = |
|
| 98 |
process_sw copy_nd.node_outputs (Corelang.add_pre_expr vl) update_out |
|
| 99 |
in |
|
| 100 |
[ |
|
| 104 | 101 |
Eq |
| 105 |
{ eq_loc = loc;
|
|
| 106 |
eq_lhs = List.map (fun v -> v.var_id) copy_nd.node_outputs; |
|
| 107 |
eq_rhs = Corelang.mkexpr loc (Expr_arrow(e_init_out, e_update_out)) |
|
| 102 |
{
|
|
| 103 |
eq_loc = loc; |
|
| 104 |
eq_lhs = List.map (fun v -> v.var_id) copy_nd.node_outputs; |
|
| 105 |
eq_rhs = Corelang.mkexpr loc (Expr_arrow (e_init_out, e_update_out)); |
|
| 108 | 106 |
}; |
| 109 | 107 |
] |
| 110 | 108 |
in |
| 111 | 109 |
let new_nd = |
| 112 |
{ copy_nd with
|
|
| 110 |
{
|
|
| 111 |
copy_nd with |
|
| 113 | 112 |
node_id = copy_nd.node_id ^ "_seal"; |
| 114 | 113 |
node_locals = m.mmemory; |
| 115 | 114 |
node_stmts = mem_eq @ output_eq; |
| ... | ... | |
| 117 | 116 |
in |
| 118 | 117 |
new_nd, orig_nd |
| 119 | 118 |
|
| 120 |
|
|
| 121 | 119 |
let funsw_to_lustre m update_out = |
| 122 | 120 |
let orig_nd = m.mname in |
| 123 | 121 |
let copy_nd = orig_nd (*Corelang.copy_node orig_nd *) in |
| 124 | 122 |
let output_eq = |
| 125 |
let e_update_out = process_sw copy_nd.node_outputs (fun x -> x) update_out in |
|
| 126 |
[ |
|
| 123 |
let e_update_out = |
|
| 124 |
process_sw copy_nd.node_outputs (fun x -> x) update_out |
|
| 125 |
in |
|
| 126 |
[ |
|
| 127 | 127 |
Eq |
| 128 |
{ eq_loc = Location.dummy_loc;
|
|
| 129 |
eq_lhs = List.map (fun v -> v.var_id) copy_nd.node_outputs; |
|
| 130 |
eq_rhs = e_update_out |
|
| 128 |
{
|
|
| 129 |
eq_loc = Location.dummy_loc; |
|
| 130 |
eq_lhs = List.map (fun v -> v.var_id) copy_nd.node_outputs; |
|
| 131 |
eq_rhs = e_update_out; |
|
| 131 | 132 |
}; |
| 132 | 133 |
] |
| 133 | 134 |
in |
| 134 | 135 |
let new_nd = |
| 135 |
{ copy_nd with
|
|
| 136 |
{
|
|
| 137 |
copy_nd with |
|
| 136 | 138 |
node_id = copy_nd.node_id ^ "_seal"; |
| 137 | 139 |
node_locals = []; |
| 138 | 140 |
node_stmts = output_eq; |
| 139 | 141 |
} |
| 140 | 142 |
in |
| 141 | 143 |
new_nd, orig_nd |
| 142 |
|
|
| 143 |
|
|
| 144 | 144 |
|
| 145 | 145 |
let to_lustre basename prog new_node orig_node = |
| 146 | 146 |
let loc = Location.dummy_loc in |
| ... | ... | |
| 156 | 156 |
in |
| 157 | 157 |
let out = open_out output_file in |
| 158 | 158 |
let fmt = Format.formatter_of_out_channel out in |
| 159 |
Format.fprintf fmt "%a@." Printers.pp_prog [new_top];
|
|
| 159 |
Format.fprintf fmt "%a@." Printers.pp_prog [ new_top ];
|
|
| 160 | 160 |
|
| 161 | 161 |
(* Verif output *) |
| 162 |
let output_file_verif = !Options.dest_dir ^ "/" ^ basename ^ "_seal_verif.lus" in |
|
| 162 |
let output_file_verif = |
|
| 163 |
!Options.dest_dir ^ "/" ^ basename ^ "_seal_verif.lus" |
|
| 164 |
in |
|
| 163 | 165 |
let out_verif = open_out output_file_verif in |
| 164 | 166 |
let fmt_verif = Format.formatter_of_out_channel out_verif in |
| 165 | 167 |
let check_nd = Lustre_utils.check_eq new_node orig_node in |
| 166 | 168 |
let check_top = |
| 167 |
Corelang.mktop_decl Location.dummy_loc output_file_verif false (Node check_nd) |
|
| 169 |
Corelang.mktop_decl Location.dummy_loc output_file_verif false |
|
| 170 |
(Node check_nd) |
|
| 168 | 171 |
in |
| 169 |
Format.fprintf fmt_verif "%a@." Printers.pp_prog (prog@[new_top;check_top]) |
|
| 170 |
|
|
| 172 |
Format.fprintf fmt_verif "%a@." Printers.pp_prog |
|
| 173 |
(prog @ [ new_top; check_top ]) |
|
| 174 |
|
|
| 171 | 175 |
let node_to_lustre basename prog m sw_init sw_step init_out update_out = |
| 172 | 176 |
let new_node, orig_nd = sw_to_lustre m sw_init sw_step init_out update_out in |
| 173 | 177 |
to_lustre basename prog new_node orig_nd |
| ... | ... | |
| 175 | 179 |
let fun_to_lustre basename prog m update_out = |
| 176 | 180 |
let new_node, orig_nd = funsw_to_lustre m update_out in |
| 177 | 181 |
to_lustre basename prog new_node orig_nd |
| 178 |
|
|
Also available in: Unified diff
reformatting