Revision ca7ff3f7
Added by Lélio Brun over 1 year 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 |
(* compile-command:"make -C .." *) |
Also available in: Unified diff
reformatting