Revision 03c767b1
Added by PierreLoï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