Revision ca7ff3f7
Added by LĂ©lio Brun 8 months ago
src/checks/stateless.ml  

13  13 
open Corelang 
14  14  
15  15 
type error = 
16 
 Stateful_kwd of ident


17 
 Stateful_imp of ident


18 
 Stateful_ext_C of ident 

16 
 Stateful_kwd of ident


17 
 Stateful_imp of ident


18 
 Stateful_ext_C of ident


19  19  
20  20 
exception Error of Location.t * error 
21  21  
22  22 
let rec check_expr expr = 
23  23 
match expr.expr_desc with 
24 
 Expr_const _ 

25 
 Expr_ident _ > true 

26 
 Expr_tuple el 

27 
 Expr_array el > List.for_all check_expr el 

28 
 Expr_access (e1, _) 

29 
 Expr_power (e1, _) > check_expr e1 

30 
 Expr_ite (c, t, e) > check_expr c && check_expr t && check_expr e 

31 
 Expr_arrow _ 

32 
 Expr_fby _ 

33 
 Expr_pre _ > false 

34 
 Expr_when (e', _, _)> check_expr e' 

35 
 Expr_merge (_, hl) > List.for_all (fun (_, h) > check_expr h) hl 

24 
 Expr_const _  Expr_ident _ > 

25 
true 

26 
 Expr_tuple el  Expr_array el > 

27 
List.for_all check_expr el 

28 
 Expr_access (e1, _)  Expr_power (e1, _) > 

29 
check_expr e1 

30 
 Expr_ite (c, t, e) > 

31 
check_expr c && check_expr t && check_expr e 

32 
 Expr_arrow _  Expr_fby _  Expr_pre _ > 

33 
false 

34 
 Expr_when (e', _, _) > 

35 
check_expr e' 

36 
 Expr_merge (_, hl) > 

37 
List.for_all (fun (_, h) > check_expr h) hl 

36  38 
 Expr_appl (i, e', i') > 
37 
let reset_opt = (match i' with None > true  Some e'' > check_expr e'') in 

38 
let stateless_node = 

39 
(Basic_library.is_stateless_fun i  ( 

40 
try 

41 
check_node (node_from_name i) 

42 
with Not_found > 

43 
let loc = expr.expr_loc in 

44 
Error.pp_error loc (fun fmt > Format.fprintf fmt "Unable to find node %s in expression %a" i Printers.pp_expr expr); 

45 
raise (Error.Error (loc, Error.Unbound_symbol i)) 

46 
)) 

47 
in 

48 
(* Warning message when trying to reset a stateless node *) 

49 
if stateless_node && not reset_opt then 

50 
Error.pp_warning expr.expr_loc (fun fmt > Format.fprintf fmt "Trying to reset call the stateless node or op %s" i) 

51 
; 

52 
check_expr e' && reset_opt && stateless_node 

53 


54 
and compute_node nd = (* returns true iff the node is stateless.*) 

39 
let reset_opt = match i' with None > true  Some e'' > check_expr e'' in 

40 
let stateless_node = 

41 
Basic_library.is_stateless_fun i 

42 
 

43 
try check_node (node_from_name i) 

44 
with Not_found > 

45 
let loc = expr.expr_loc in 

46 
Error.pp_error loc (fun fmt > 

47 
Format.fprintf fmt "Unable to find node %s in expression %a" i 

48 
Printers.pp_expr expr); 

49 
raise (Error.Error (loc, Error.Unbound_symbol i)) 

50 
in 

51 
(* Warning message when trying to reset a stateless node *) 

52 
if stateless_node && not reset_opt then 

53 
Error.pp_warning expr.expr_loc (fun fmt > 

54 
Format.fprintf fmt "Trying to reset call the stateless node or op %s" 

55 
i); 

56 
check_expr e' && reset_opt && stateless_node 

57  
58 
and compute_node nd = 

59 
(* returns true iff the node is stateless.*) 

55  60 
let eqs, aut = get_node_eqs nd in 
56 
aut = [] && (* A node containinig an automaton will be stateful *) 

57 
List.for_all (fun eq > check_expr eq.eq_rhs) eqs 

61 
aut = [] 

62 
&& (* A node containinig an automaton will be stateful *) 

63 
List.for_all (fun eq > check_expr eq.eq_rhs) eqs 

64  
58  65 
and check_node td = 
59 
match td.top_decl_desc with


60 
 Node nd > (


66 
match td.top_decl_desc with 

67 
 Node nd > ( 

61  68 
match nd.node_stateless with 
62 
 None > 

63 
begin 

64 
let stateless = compute_node nd in 

65 
nd.node_stateless < Some stateless; 

66 
if nd.node_dec_stateless && (not stateless) 

67 
then raise (Error (td.top_decl_loc, Stateful_kwd nd.node_id)) 

68 
else (nd.node_dec_stateless < stateless; stateless) 

69 
end 

70 
 Some stl > stl) 

69 
 None > 

70 
let stateless = compute_node nd in 

71 
nd.node_stateless < Some stateless; 

72 
if nd.node_dec_stateless && not stateless then 

73 
raise (Error (td.top_decl_loc, Stateful_kwd nd.node_id)) 

74 
else ( 

75 
nd.node_dec_stateless < stateless; 

76 
stateless) 

77 
 Some stl > 

78 
stl) 

71  79 
 ImportedNode nd > 
72 
begin 

73 
(if nd.nodei_prototype = Some "C" && not nd.nodei_stateless 

74 
then raise (Error (td.top_decl_loc, Stateful_ext_C nd.nodei_id))); 

75 
nd.nodei_stateless 

76 
end 

77 
 _ > true 

78  
79 
let check_prog decls = 

80 
List.iter (fun td > ignore (check_node td)) decls 

80 
if nd.nodei_prototype = Some "C" && not nd.nodei_stateless then 

81 
raise (Error (td.top_decl_loc, Stateful_ext_C nd.nodei_id)); 

82 
nd.nodei_stateless 

83 
 _ > 

84 
true 

81  85  
86 
let check_prog decls = List.iter (fun td > ignore (check_node td)) decls 

82  87  
83  88 
let force_prog decls = 
84  89 
let force_node td = 
85 
match td.top_decl_desc with


86 
 Node nd > (


90 
match td.top_decl_desc with 

91 
 Node nd >


87  92 
nd.node_dec_stateless < false; 
88 
nd.node_stateless < Some false) 

89 
 _ > () 

93 
nd.node_stateless < Some false 

94 
 _ > 

95 
() 

90  96 
in 
91  97 
List.iter (fun td > ignore (force_node td)) decls 
92  98  
93  99 
let check_compat_decl decl = 
94  100 
match decl.top_decl_desc with 
95 
 ImportedNode nd > (* A node declared in the header (lusi) shall


96 
be locally defined with compatible stateless


97 
flag *)


98 
begin


99 
let td = Corelang.node_from_name nd.nodei_id in


100 
(match td.top_decl_desc with


101 
 Node nd' > let stateless = check_node td in


102 
if nd.nodei_stateless && (not stateless)


103 
then raise (Error (td.top_decl_loc, Stateful_imp nd.nodei_id))


104 
else nd'.node_dec_stateless < nd.nodei_stateless


105 
 _ > assert false)


106 
end


101 
 ImportedNode nd > ( 

102 
(* A node declared in the header (lusi) shall be locally defined with


103 
compatible stateless flag *)


104 
let td = Corelang.node_from_name nd.nodei_id in


105 
match td.top_decl_desc with


106 
 Node nd' >


107 
let stateless = check_node td in 

108 
if nd.nodei_stateless && not stateless then


109 
raise (Error (td.top_decl_loc, Stateful_imp nd.nodei_id))


110 
else nd'.node_dec_stateless < nd.nodei_stateless 

111 
 _ >


112 
assert false)


107  113 
 Node nd > ( 
108 
match nd.node_spec with 

109 
Some (Contract _) > (* A contract element in a header does not 

110 
need to be provided in the associed lus 

111 
file *) 

112 
() 

113 
 _ > assert false) 

114 


115 
 _ > () 

114 
match nd.node_spec with 

115 
 Some (Contract _) > 

116 
(* A contract element in a header does not need to be provided in the 

117 
associed lus file *) 

118 
() 

119 
 _ > 

120 
assert false) 

121 
 _ > 

122 
() 

116  123  
117 
let check_compat header = 

118 
List.iter check_compat_decl header 

124 
let check_compat header = List.iter check_compat_decl header 

119  125  
120  126 
let pp_error fmt err = 
121  127 
match err with 
122  128 
 Stateful_kwd nd > 
123 
Format.fprintf fmt 

124 
"node %s should be stateless but is actually stateful.@." 

125 
nd 

129 
Format.fprintf fmt "node %s should be stateless but is actually stateful.@." 

130 
nd 

126  131 
 Stateful_imp nd > 
127 
Format.fprintf fmt 

128 
"node %s is declared stateless but is actually stateful.@." 

129 
nd 

132 
Format.fprintf fmt 

133 
"node %s is declared stateless but is actually stateful.@." nd 

130  134 
 Stateful_ext_C nd > 
131 
Format.fprintf fmt 

132 
"node %s with declared prototype C cannot be stateful, it has to be a function.@." 

133 
nd 

135 
Format.fprintf fmt 

136 
"node %s with declared prototype C cannot be stateful, it has to be a \ 

137 
function.@." 

138 
nd 

134  139  
135  140 
(* Local Variables: *) 
136  141 
(* compilecommand:"make C .." *) 
Also available in: Unified diff
reformatting