Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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
(* compile-command:"make -C .." *)
130
(* End: *)