Project

General

Profile

Download (4.56 KB) Statistics
| Branch: | Tag: | Revision:
1 a2d97a3e ploc
(********************************************************************)
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 8446bf03 ploc
open Lustre_types
13 e135421f xthirioux
open Corelang
14
15
type error =
16 ca7ff3f7 Lélio Brun
  | Stateful_kwd of ident
17
  | Stateful_imp of ident
18
  | Stateful_ext_C of ident
19 e135421f xthirioux
20
exception Error of Location.t * error
21
22
let rec check_expr expr =
23
  match expr.expr_desc with
24 ca7ff3f7 Lélio Brun
  | 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
38 e135421f xthirioux
  | Expr_appl (i, e', i') ->
39 ca7ff3f7 Lélio Brun
    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.*)
60 333e3a25 ploc
  let eqs, aut = get_node_eqs nd in
61 ca7ff3f7 Lélio Brun
  aut = []
62
  && (* A node containinig an automaton will be stateful *)
63
  List.for_all (fun eq -> check_expr eq.eq_rhs) eqs
64
65 e135421f xthirioux
and check_node td =
66 ca7ff3f7 Lélio Brun
  match td.top_decl_desc with
67
  | Node nd -> (
68 e135421f xthirioux
    match nd.node_stateless with
69 ca7ff3f7 Lélio Brun
    | 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)
79 04a63d25 xthirioux
  | ImportedNode nd ->
80 ca7ff3f7 Lélio Brun
    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
85 e135421f xthirioux
86 ca7ff3f7 Lélio Brun
let check_prog decls = List.iter (fun td -> ignore (check_node td)) decls
87 04a63d25 xthirioux
88
let force_prog decls =
89
  let force_node td =
90 ca7ff3f7 Lélio Brun
    match td.top_decl_desc with
91
    | Node nd ->
92 04a63d25 xthirioux
      nd.node_dec_stateless <- false;
93 ca7ff3f7 Lélio Brun
      nd.node_stateless <- Some false
94
    | _ ->
95
      ()
96 04a63d25 xthirioux
  in
97
  List.iter (fun td -> ignore (force_node td)) decls
98
99 e135421f xthirioux
let check_compat_decl decl =
100 f4cba4b8 ploc
  match decl.top_decl_desc with
101 ca7ff3f7 Lélio Brun
  | 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)
113 f4cba4b8 ploc
  | Node nd -> (
114 ca7ff3f7 Lélio Brun
    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
    ()
123 e135421f xthirioux
124 ca7ff3f7 Lélio Brun
let check_compat header = List.iter check_compat_decl header
125 e135421f xthirioux
126
let pp_error fmt err =
127
  match err with
128
  | Stateful_kwd nd ->
129 ca7ff3f7 Lélio Brun
    Format.fprintf fmt "node %s should be stateless but is actually stateful.@."
130
      nd
131 e135421f xthirioux
  | Stateful_imp nd ->
132 ca7ff3f7 Lélio Brun
    Format.fprintf fmt
133
      "node %s is declared stateless but is actually stateful.@." nd
134 04a63d25 xthirioux
  | Stateful_ext_C nd ->
135 ca7ff3f7 Lélio Brun
    Format.fprintf fmt
136
      "node %s with declared prototype C cannot be stateful, it has to be a \
137
       function.@."
138
      nd
139 e135421f xthirioux
140
(* Local Variables: *)
141
(* compile-command:"make -C .." *)
142
(* End: *)