## lustrec/src/checks/stateless.ml @ ca7ff3f7

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: *)
``` |