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

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