lustrec / src / checks / stateless.ml @ 04a188ec
History  View  Annotate  Download (4.34 KB)
1 
(********************************************************************) 

2 
(* *) 
3 
(* The LustreC compiler toolset / The LustreC Development Team *) 
4 
(* Copyright 2012   ONERA  CNRS  INPT *) 
5 
(* *) 
6 
(* LustreC is free software, distributed WITHOUT ANY WARRANTY *) 
7 
(* under the terms of the GNU Lesser General Public License *) 
8 
(* version 2.1. *) 
9 
(* *) 
10 
(********************************************************************) 
11  
12 
open Lustre_types 
13 
open Corelang 
14  
15 
type error = 
16 
 Stateful_kwd of ident 
17 
 Stateful_imp of ident 
18 
 Stateful_ext_C of ident 
19  
20 
exception Error of Location.t * error 
21  
22 
let rec check_expr expr = 
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', i, l)> check_expr e' 
35 
 Expr_merge (i, hl) > List.for_all (fun (t, h) > check_expr h) hl 
36 
 Expr_appl (i, e', i') > 
37 
check_expr e' && 
38 
(Basic_library.is_stateless_fun i  ( 
39 
try 
40 
check_node (node_from_name i) 
41 
with Not_found > 
42 
let loc = expr.expr_loc in 
43 
Error.pp_error loc (fun fmt > Format.fprintf fmt "Unable to find node %s in expression %a" i Printers.pp_expr expr); 
44 
raise (Error.Error (loc, Error.Unbound_symbol i)) 
45 
)) 
46 

47 
and compute_node nd = (* returns true iff the node is stateless.*) 
48 
let eqs, aut = get_node_eqs nd in 
49 
aut = [] && (* A node containinig an automaton will be stateful *) 
50 
List.for_all (fun eq > check_expr eq.eq_rhs) eqs 
51 
and check_node td = 
52 
match td.top_decl_desc with 
53 
 Node nd > ( 
54 
match nd.node_stateless with 
55 
 None > 
56 
begin 
57 
let stateless = compute_node nd in 
58 
nd.node_stateless < Some stateless; 
59 
if nd.node_dec_stateless && (not stateless) 
60 
then raise (Error (td.top_decl_loc, Stateful_kwd nd.node_id)) 
61 
else (nd.node_dec_stateless < stateless; stateless) 
62 
end 
63 
 Some stl > stl) 
64 
 ImportedNode nd > 
65 
begin 
66 
(if nd.nodei_prototype = Some "C" && not nd.nodei_stateless 
67 
then raise (Error (td.top_decl_loc, Stateful_ext_C nd.nodei_id))); 
68 
nd.nodei_stateless 
69 
end 
70 
 _ > true 
71  
72 
let check_prog decls = 
73 
List.iter (fun td > ignore (check_node td)) decls 
74  
75  
76 
let force_prog decls = 
77 
let force_node td = 
78 
match td.top_decl_desc with 
79 
 Node nd > ( 
80 
nd.node_dec_stateless < false; 
81 
nd.node_stateless < Some false) 
82 
 _ > () 
83 
in 
84 
List.iter (fun td > ignore (force_node td)) decls 
85  
86 
let check_compat_decl decl = 
87 
match decl.top_decl_desc with 
88 
 ImportedNode nd > (* A node declared in the header (lusi) shall 
89 
be locally defined with compatible stateless 
90 
flag *) 
91 
begin 
92 
let td = Corelang.node_from_name nd.nodei_id in 
93 
(match td.top_decl_desc with 
94 
 Node nd' > let stateless = check_node td in 
95 
if nd.nodei_stateless && (not stateless) 
96 
then raise (Error (td.top_decl_loc, Stateful_imp nd.nodei_id)) 
97 
else nd'.node_dec_stateless < nd.nodei_stateless 
98 
 _ > assert false) 
99 
end 
100 
 Node nd > ( 
101 
match nd.node_spec with 
102 
Some (Contract _) > (* A contract element in a header does not 
103 
need to be provided in the associed lus 
104 
file *) 
105 
() 
106 
 _ > assert false) 
107 

108 
 _ > () 
109  
110 
let check_compat header = 
111 
List.iter check_compat_decl header 
112  
113 
let pp_error fmt err = 
114 
match err with 
115 
 Stateful_kwd nd > 
116 
Format.fprintf fmt 
117 
"node %s should be stateless but is actually stateful.@." 
118 
nd 
119 
 Stateful_imp nd > 
120 
Format.fprintf fmt 
121 
"node %s is declared stateless but is actually stateful.@." 
122 
nd 
123 
 Stateful_ext_C nd > 
124 
Format.fprintf fmt 
125 
"node %s with declared prototype C cannot be stateful, it has to be a function.@." 
126 
nd 
127  
128 
(* Local Variables: *) 
129 
(* compilecommand:"make C .." *) 
130 
(* End: *) 