Project

General

Profile

Download (4.56 KB) Statistics
| Branch: | Tag: | Revision:
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 _ | 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
  | Expr_appl (i, e', i') ->
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.*)
60
  let eqs, aut = get_node_eqs nd in
61
  aut = []
62
  && (* A node containinig an automaton will be stateful *)
63
  List.for_all (fun eq -> check_expr eq.eq_rhs) eqs
64

    
65
and check_node td =
66
  match td.top_decl_desc with
67
  | Node nd -> (
68
    match nd.node_stateless with
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)
79
  | ImportedNode nd ->
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
85

    
86
let check_prog decls = List.iter (fun td -> ignore (check_node td)) decls
87

    
88
let force_prog decls =
89
  let force_node td =
90
    match td.top_decl_desc with
91
    | Node nd ->
92
      nd.node_dec_stateless <- false;
93
      nd.node_stateless <- Some false
94
    | _ ->
95
      ()
96
  in
97
  List.iter (fun td -> ignore (force_node td)) decls
98

    
99
let check_compat_decl decl =
100
  match decl.top_decl_desc with
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)
113
  | Node nd -> (
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
    ()
123

    
124
let check_compat header = List.iter check_compat_decl header
125

    
126
let pp_error fmt err =
127
  match err with
128
  | Stateful_kwd nd ->
129
    Format.fprintf fmt "node %s should be stateless but is actually stateful.@."
130
      nd
131
  | Stateful_imp nd ->
132
    Format.fprintf fmt
133
      "node %s is declared stateless but is actually stateful.@." nd
134
  | Stateful_ext_C nd ->
135
    Format.fprintf fmt
136
      "node %s with declared prototype C cannot be stateful, it has to be a \
137
       function.@."
138
      nd
139

    
140
(* Local Variables: *)
141
(* compile-command:"make -C .." *)
142
(* End: *)
(5-5/5)