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

let reset_opt = (match i' with None > true  Some e'' > check_expr e'') in

38

let stateless_node =

39

(Basic_library.is_stateless_fun i  (

40

try

41

check_node (node_from_name i)

42

with Not_found >

43

let loc = expr.expr_loc in

44

Error.pp_error loc (fun fmt > Format.fprintf fmt "Unable to find node %s in expression %a" i Printers.pp_expr expr);

45

raise (Error.Error (loc, Error.Unbound_symbol i))

46

))

47

in

48

(* Warning message when trying to reset a stateless node *)

49

if stateless_node && not reset_opt then

50

Error.pp_warning expr.expr_loc (fun fmt > Format.fprintf fmt "Trying to reset call the stateless node or op %s" i)

51

;

52

check_expr e' && reset_opt && stateless_node

53


54

and compute_node nd = (* returns true iff the node is stateless.*)

55

let eqs, aut = get_node_eqs nd in

56

aut = [] && (* A node containinig an automaton will be stateful *)

57

List.for_all (fun eq > check_expr eq.eq_rhs) eqs

58

and check_node td =

59

match td.top_decl_desc with

60

 Node nd > (

61

match nd.node_stateless with

62

 None >

63

begin

64

let stateless = compute_node nd in

65

nd.node_stateless < Some stateless;

66

if nd.node_dec_stateless && (not stateless)

67

then raise (Error (td.top_decl_loc, Stateful_kwd nd.node_id))

68

else (nd.node_dec_stateless < stateless; stateless)

69

end

70

 Some stl > stl)

71

 ImportedNode nd >

72

begin

73

(if nd.nodei_prototype = Some "C" && not nd.nodei_stateless

74

then raise (Error (td.top_decl_loc, Stateful_ext_C nd.nodei_id)));

75

nd.nodei_stateless

76

end

77

 _ > true

78


79

let check_prog decls =

80

List.iter (fun td > ignore (check_node td)) decls

81


82


83

let force_prog decls =

84

let force_node td =

85

match td.top_decl_desc with

86

 Node nd > (

87

nd.node_dec_stateless < false;

88

nd.node_stateless < Some false)

89

 _ > ()

90

in

91

List.iter (fun td > ignore (force_node td)) decls

92


93

let check_compat_decl decl =

94

match decl.top_decl_desc with

95

 ImportedNode nd > (* A node declared in the header (lusi) shall

96

be locally defined with compatible stateless

97

flag *)

98

begin

99

let td = Corelang.node_from_name nd.nodei_id in

100

(match td.top_decl_desc with

101

 Node nd' > let stateless = check_node td in

102

if nd.nodei_stateless && (not stateless)

103

then raise (Error (td.top_decl_loc, Stateful_imp nd.nodei_id))

104

else nd'.node_dec_stateless < nd.nodei_stateless

105

 _ > assert false)

106

end

107

 Node nd > (

108

match nd.node_spec with

109

Some (Contract _) > (* A contract element in a header does not

110

need to be provided in the associed lus

111

file *)

112

()

113

 _ > assert false)

114


115

 _ > ()

116


117

let check_compat header =

118

List.iter check_compat_decl header

119


120

let pp_error fmt err =

121

match err with

122

 Stateful_kwd nd >

123

Format.fprintf fmt

124

"node %s should be stateless but is actually stateful.@."

125

nd

126

 Stateful_imp nd >

127

Format.fprintf fmt

128

"node %s is declared stateless but is actually stateful.@."

129

nd

130

 Stateful_ext_C nd >

131

Format.fprintf fmt

132

"node %s with declared prototype C cannot be stateful, it has to be a function.@."

133

nd

134


135

(* Local Variables: *)

136

(* compilecommand:"make C .." *)

137

(* End: *)
