Project

General

Profile

Revision 8446bf03

View differences:

Makefile.in
59 59

  
60 60
%.lusic: %.lusi
61 61
	@echo Compiling $<
62
	@$(LOCAL_BINDIR)/lustrec -verbose 0 -d include $<
62
	@$(LOCAL_BINDIR)/lustrec -verbose 0 -I include -d include $<
63 63

  
64 64
clean-lusic:
65 65
	@rm -f $(LUSI_LIBS:%.lusi=%.lusic)
src/access.ml
19 19
open Utils
20 20
(* Yes, opening both modules is dirty as some type names will be
21 21
   overwritten, yet this makes notations far lighter.*)
22
open LustreSpec
22
open Lustre_types
23 23
open Corelang
24 24
open Types
25 25
open Format
src/algebraicLoop.ml
11 11
   If the option solve_al is activated, the resulting partially inlined prog is
12 12
   propagated fur future processing Otherwise the compilation stops
13 13
*)
14
open LustreSpec
14
open Lustre_types
15 15
open Corelang
16 16
open Utils
17 17

  
src/annotations.ml
9 9
(*                                                                  *)
10 10
(********************************************************************)
11 11

  
12
open LustreSpec
12
open Lustre_types
13 13

  
14 14

  
15 15
(* Associate to each annotation key the pair (node, expr tag) *)
src/automata.ml
10 10
(********************************************************************)
11 11

  
12 12
open Utils
13
open LustreSpec
13
open Lustre_types
14 14
open Corelang
15 15

  
16 16

  
src/backends/C/c_backend_common.ml
10 10
(********************************************************************)
11 11

  
12 12
open Format
13
open LustreSpec
13
open Lustre_types
14 14
open Corelang
15 15
open Machine_code
16 16

  
......
194 194
   but an offset suffix may be added for array variables
195 195
*)
196 196
let rec pp_c_val self pp_var fmt v =
197
  let open Machine_code_types in
197 198
  match v.value_desc with
198 199
  | Cst c         -> pp_c_const fmt c
199 200
  | Array vl      -> fprintf fmt "{%a}" (Utils.fprintf_list ~sep:", " (pp_c_val self pp_var)) vl
......
462 463
  else
463 464
    fprintf fmt "&%s" id.var_id
464 465

  
465
let pp_main_call mname self fmt m (inputs: value_t list) (outputs: var_decl list) =
466
let pp_main_call mname self fmt m (inputs: Machine_code_types.value_t list) (outputs: var_decl list) =
466 467
  if fst (get_stateless_status m)
467 468
  then
468 469
    fprintf fmt "%a (%a%t%a);"
......
480 481
      self
481 482

  
482 483
let pp_c_var m self pp_var fmt var =
484
  let open Machine_code_types in
483 485
  if is_memory m var
484 486
  then
485 487
    pp_c_val self pp_var fmt (mk_val (StateVar var) var.var_type)
......
516 518
    end
517 519

  
518 520
let pp_const_initialize pp_var fmt const =
521
  let open Machine_code_types in
519 522
  let var = mk_val (LocalVar (Corelang.var_decl_of_const const)) const.const_type in
520 523
  let rec aux indices value fmt typ =
521 524
    if Types.is_array_type typ
......
594 597
      aux [] fmt var.var_type
595 598
    end
596 599

  
597
let pp_call m self pp_read pp_write fmt i (inputs: value_t list) (outputs: var_decl list) =
600
let pp_call m self pp_read pp_write fmt i (inputs: Machine_code_types.value_t list) (outputs: var_decl list) =
598 601
 try (* stateful node instance *)
599 602
   let (n,_) = List.assoc i m.minstances in
600 603
   fprintf fmt "%a (%a%t%a%t%s->%s);"
......
613 616
     (Utils.pp_final_char_if_non_empty ", " inputs) 
614 617
     (Utils.fprintf_list ~sep:", " pp_write) outputs 
615 618

  
616
let pp_basic_instance_call m self fmt i (inputs: value_t list) (outputs: var_decl list) =
619
let pp_basic_instance_call m self fmt i (inputs: Machine_code_types.value_t list) (outputs: var_decl list) =
617 620
  pp_call m self (pp_c_var_read m) (pp_c_var_write m) fmt i inputs outputs
618 621
(*
619 622
 try (* stateful node instance *)
......
635 638
     (Utils.fprintf_list ~sep:", " (pp_c_var_write m)) outputs 
636 639
*)
637 640

  
638
let pp_instance_call m self fmt i (inputs: value_t list) (outputs: var_decl list) =
641
let pp_instance_call m self fmt i (inputs: Machine_code_types.value_t list) (outputs: var_decl list) =
639 642
  let pp_offset pp_var indices fmt var =
640 643
    match indices with
641 644
    | [] -> fprintf fmt "%a" pp_var var
......
655 658
  in
656 659
  begin
657 660
    reset_loop_counter ();
658
    aux [] fmt (List.hd inputs).value_type
661
    aux [] fmt (List.hd inputs).Machine_code_types.value_type
659 662
  end
660 663

  
661 664
  (*** Common functions for main ***)
src/backends/C/c_backend_header.ml
10 10
(********************************************************************)
11 11

  
12 12
open Format 
13
open LustreSpec
13
open Lustre_types
14 14
open Corelang
15 15
open Machine_code
16 16
open C_backend_common
......
51 51
  end
52 52

  
53 53
let rec print_static_val pp_var fmt v =
54
  let open Machine_code_types in
54 55
  match v.value_desc with
55 56
  | Cst c         -> pp_c_const fmt c
56 57
  | LocalVar v    -> pp_var fmt v
src/backends/C/c_backend_main.ml
9 9
(*                                                                  *)
10 10
(********************************************************************)
11 11

  
12
open LustreSpec
12
open Lustre_types
13
open Machine_code_types
13 14
open Corelang
14 15
open Machine_code
15 16
open Format
src/backends/C/c_backend_makefile.ml
10 10
(********************************************************************)
11 11

  
12 12
open Format
13
open LustreSpec
13
open Lustre_types
14 14
open Corelang
15 15

  
16 16
let pp_dep fmt (Dep(b,id,tops,stateful)) =
src/backends/C/c_backend_mauve.ml
1
open LustreSpec
1
open Lustre_types
2 2
open Corelang
3 3
open Machine_code
4 4
open Format
src/backends/C/c_backend_spec.ml
10 10
(********************************************************************)
11 11

  
12 12
open Format
13
open LustreSpec
13
open Lustre_types
14 14
open Machine_code
15 15
open C_backend_common
16 16
open Utils
src/backends/C/c_backend_src.ml
10 10
(********************************************************************)
11 11

  
12 12
open Format
13
open LustreSpec
13
open Lustre_types
14
open Machine_code_types
14 15
open Corelang
15 16
open Machine_code
16 17
open C_backend_common
src/backends/EMF/EMF_backend.ml
98 98

  
99 99
*)
100 100

  
101
open LustreSpec
101
open Lustre_types
102
open Machine_code_types
102 103
open Machine_code
103 104
open Format 
104 105
open EMF_common
src/backends/EMF/EMF_common.ml
1
open LustreSpec
1
open Lustre_types
2
open Machine_code_types
3

  
2 4
open Format
3 5
open Machine_code 
4 6

  
src/backends/EMF/EMF_library_calls.ml
3 3
    moment, modular compilation of multiple lustre sources as one output JSON is not
4 4
    considered. *)
5 5

  
6
open LustreSpec
6
open Lustre_types
7 7
open Machine_code
8 8
open Format
9 9
open EMF_common
src/backends/Horn/horn_backend.ml
16 16
*)
17 17

  
18 18
open Format
19
open LustreSpec
19
open Lustre_types
20 20
open Corelang
21 21
open Machine_code
22 22

  
src/backends/Horn/horn_backend_collecting_sem.ml
16 16
*)
17 17

  
18 18
open Format
19
open LustreSpec
19
open Lustre_types
20 20
open Corelang
21 21
open Machine_code
22 22

  
src/backends/Horn/horn_backend_common.ml
10 10
(********************************************************************)
11 11

  
12 12
open Format
13
open LustreSpec
13
open Lustre_types
14 14
open Corelang
15 15
open Machine_code
16 16

  
......
108 108
  aux true machine.mname.node_id machine
109 109

  
110 110
(* Extract the arrows of a given node/machine *)
111
let arrow_vars machines machine : LustreSpec.var_decl list =
111
let arrow_vars machines machine : Lustre_types.var_decl list =
112 112
  let rec aux fst prefix m =
113 113
    List.fold_left (fun accu (id, (n, _)) ->
114 114
      let name = node_name n in
src/backends/Horn/horn_backend_printers.ml
16 16
*)
17 17

  
18 18
open Format
19
open LustreSpec
19
open Lustre_types
20
open Machine_code_types
20 21
open Corelang
21 22
open Machine_code
22 23

  
src/backends/Horn/horn_backend_traces.ml
16 16
*)
17 17

  
18 18
open Format
19
open LustreSpec
19
open Lustre_types
20 20
open Corelang
21 21
open Machine_code
22 22

  
src/basic_library.ml
11 11

  
12 12
(* Parts of this file come from the Prelude compiler *)
13 13

  
14
open LustreSpec
14
(*open LustreSpec*)
15 15
open Type_predef
16 16
open Clock_predef
17 17
open Delay_predef
......
126 126
  | _                               -> List.mem x internal_funs
127 127

  
128 128
let is_expr_internal_fun expr =
129
  let open Lustre_types in
129 130
  match expr.expr_desc with
130 131
  | Expr_appl (f, e, _) -> is_internal_fun f (Types.type_list_of_type e.expr_type)
131 132
  | _                   -> assert false
132 133

  
133 134
let is_value_internal_fun v =
135
  let open Machine_code_types in
134 136
  match v.value_desc with
135 137
  | Fun (f, vl) -> is_internal_fun f (List.map (fun v -> v.value_type) vl)
136 138
  | _           -> assert false
src/causality.ml
15 15
(** Simple modular syntactic causality analysis. Can reject correct
16 16
    programs, especially if the program is not flattened first. *)
17 17
open Utils
18
open LustreSpec
18
open Lustre_types
19 19
open Corelang
20 20
open Graph
21 21

  
src/clock_calculus.ml
19 19
    is shared.  Simple environments, very limited identifier scoping, no
20 20
    identifier redefinition allowed. *)
21 21
open Utils
22
open LustreSpec
22
open Lustre_types
23 23
open Corelang
24 24
open Clocks
25 25
open Format
src/compiler_common.ml
11 11

  
12 12
open Utils
13 13
open Format 
14
open LustreSpec
14
open Lustre_types
15 15
open Corelang
16 16

  
17 17
let check_main () =
src/compiler_stages.ml
1 1
open Format
2 2
open Utils
3 3
open Compiler_common
4
open LustreSpec
4
open Lustre_types
5 5

  
6 6
exception StopPhase1 of program
7 7

  
src/corelang.ml
10 10
(********************************************************************)
11 11

  
12 12
open Format
13
open LustreSpec
13
open Lustre_types
14
open Machine_code_types
14 15
(*open Dimension*)
15 16

  
16 17

  
src/corelang.mli
10 10
(********************************************************************)
11 11

  
12 12

  
13
open LustreSpec
13
open Lustre_types
14 14

  
15 15
exception Error of Location.t * Error.error_kind
16 16
module VSet: Set.S
......
29 29
    string option (* parent id *)
30 30
  -> var_decl
31 31

  
32
val var_decl_of_const: ?parentid:LustreSpec.ident option -> const_desc -> var_decl
32
val var_decl_of_const: ?parentid:ident option -> const_desc -> var_decl
33 33
val mkexpr: Location.t ->  expr_desc -> expr
34 34
val mkeq: Location.t -> ident list * expr -> eq
35 35
val mkassert: Location.t -> expr -> assert_t
......
40 40
val mktop: top_decl_desc -> top_decl
41 41

  
42 42
(* constructor for machine types *)
43
val mkinstr: ?lustre_expr:expr -> ?lustre_eq: eq -> instr_t_desc -> instr_t
44
val get_instr_desc: instr_t -> instr_t_desc
45
val update_instr_desc: instr_t -> instr_t_desc -> instr_t
43
val mkinstr: ?lustre_expr:expr -> ?lustre_eq: eq -> Machine_code_types.instr_t_desc -> Machine_code_types.instr_t
44
val get_instr_desc: Machine_code_types.instr_t -> Machine_code_types.instr_t_desc
45
val update_instr_desc: Machine_code_types.instr_t -> Machine_code_types.instr_t_desc -> Machine_code_types.instr_t
46 46
  
47 47
val node_table : (ident, top_decl) Hashtbl.t
48 48
val print_node_table:  Format.formatter -> unit -> unit
src/error.ml
1 1
open Format
2 2

  
3
type ident = LustreSpec.ident
3
type ident = Lustre_types.ident
4 4
type error_kind =
5 5
    Main_not_found
6 6
  | Main_wrong_kind
src/features/machine_types/machine_types.ml
37 37
     propager les types machines aux variables fraiches creees par la normalisation
38 38

  
39 39
*)
40
open LustreSpec
40
open Lustre_types
41 41

  
42 42
let is_active = false
43 43
  
src/inliner.ml
9 9
(*                                                                  *)
10 10
(********************************************************************)
11 11

  
12
open LustreSpec
12
open Lustre_types
13 13
open Corelang
14 14
open Utils
15 15

  
src/liveness.ml
10 10
(********************************************************************)
11 11

  
12 12
open Utils
13
open LustreSpec
13
open Lustre_types
14 14
open Corelang
15 15
open Graph
16 16
open Causality
src/lusic.ml
11 11
(********************************************************************)
12 12

  
13 13
open Format 
14
open LustreSpec
14
open Lustre_types
15 15
open Corelang
16 16

  
17 17
(********************************************************************************************)
src/lustreSpec.ml
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
type ident = Utils.ident
13
type rat = Utils.rat
14
type tag = Utils.tag
15
type label = Utils.ident
16

  
17
type type_dec =
18
    {ty_dec_desc: type_dec_desc;
19
     ty_dec_loc: Location.t}
20

  
21
and type_dec_desc =
22
  | Tydec_any
23
  | Tydec_int
24
  | Tydec_real
25
  (* | Tydec_float *)
26
  | Tydec_bool
27
  | Tydec_clock of type_dec_desc
28
  | Tydec_const of ident
29
  | Tydec_enum of ident list
30
  | Tydec_struct of (ident * type_dec_desc) list
31
  | Tydec_array of Dimension.dim_expr * type_dec_desc
32

  
33
type typedec_desc =
34
    {tydec_id: ident}
35

  
36
type typedef_desc =
37
    {tydef_id: ident;
38
     tydef_desc: type_dec_desc}
39

  
40
type clock_dec =
41
    {ck_dec_desc: clock_dec_desc;
42
     ck_dec_loc: Location.t}
43

  
44
and clock_dec_desc =
45
  | Ckdec_any
46
  | Ckdec_bool of (ident * ident) list
47

  
48

  
49
type constant =
50
  | Const_int of int
51
  | Const_real of Num.num * int * string (* (a, b, c) means a * 10^-b. c is the original string *)
52
  | Const_array of constant list
53
  | Const_tag of label
54
  | Const_string of string (* used only for annotations *)
55
  | Const_struct of (label * constant) list
56

  
57
type quantifier_type = Exists | Forall
58

  
59
type var_decl =
60
    {var_id: ident;
61
     var_orig:bool;
62
     var_dec_type: type_dec;
63
     var_dec_clock: clock_dec;
64
     var_dec_const: bool;
65
     var_dec_value: expr option;
66
     mutable var_parent_nodeid: ident option;
67
     mutable var_type: Types.type_expr;
68
     mutable var_clock: Clocks.clock_expr;
69
     var_loc: Location.t}
70

  
71
(** The core language and its ast. Every element of the ast contains its
72
    location in the program text. The type and clock of an ast element
73
    is mutable (and initialized to dummy values). This avoids to have to
74
    duplicate ast structures (e.g. ast, typed_ast, clocked_ast). *)
75

  
76

  
77

  
78
(* The tag of an expression is a unique identifier used to distinguish
79
   different instances of the same node *)
80
and expr =
81
    {expr_tag: tag;
82
     expr_desc: expr_desc;
83
     mutable expr_type: Types.type_expr;
84
     mutable expr_clock: Clocks.clock_expr;
85
     mutable expr_delay: Delay.delay_expr;
86
     mutable expr_annot: expr_annot option;
87
     expr_loc: Location.t}
88

  
89
and expr_desc =
90
  | Expr_const of constant
91
  | Expr_ident of ident
92
  | Expr_tuple of expr list
93
  | Expr_ite   of expr * expr * expr
94
  | Expr_arrow of expr * expr
95
  | Expr_fby of expr * expr
96
  | Expr_array of expr list
97
  | Expr_access of expr * Dimension.dim_expr
98
  | Expr_power of expr * Dimension.dim_expr
99
  | Expr_pre of expr
100
  | Expr_when of expr * ident * label
101
  | Expr_merge of ident * (label * expr) list
102
  | Expr_appl of call_t
103

  
104
and call_t = ident * expr * expr option
105
     (* The third part denotes the boolean condition for resetting *)
106

  
107
and eq =
108
    {eq_lhs: ident list;
109
     eq_rhs: expr;
110
     eq_loc: Location.t}
111

  
112
  (* The tag of an expression is a unique identifier used to distinguish
113
     different instances of the same node *)
114
and  eexpr =
115
    {eexpr_tag: tag;
116
     eexpr_qfexpr: expr;
117
     eexpr_quantifiers: (quantifier_type * var_decl list) list;
118
     mutable eexpr_type: Types.type_expr;
119
     mutable eexpr_clock: Clocks.clock_expr;
120
     mutable eexpr_normalized: (var_decl * eq list * var_decl list) option;
121
     eexpr_loc: Location.t}
122

  
123
and expr_annot =
124
 {annots: (string list * eexpr) list;
125
  annot_loc: Location.t}
126

  
127
type node_annot = {
128
  requires: eexpr list;
129
  ensures: eexpr list;
130
  behaviors: (string * eexpr list * eexpr list * Location.t) list;
131
  spec_loc: Location.t;
132
}
133

  
134
type offset =
135
| Index of Dimension.dim_expr
136
| Field of label
137

  
138
type assert_t =
139
    {
140
      assert_expr: expr;
141
      assert_loc: Location.t;
142
    }
143

  
144
type statement =
145
| Eq of eq
146
| Aut of automata_desc
147

  
148
and automata_desc =
149
  {aut_id : ident;
150
   aut_handlers: handler_desc list;
151
   aut_loc: Location.t}
152

  
153
and handler_desc =
154
  {hand_state: ident;
155
   hand_unless: (Location.t * expr * bool * ident) list;
156
   hand_until: (Location.t * expr * bool * ident) list;
157
   hand_locals: var_decl list;
158
   hand_stmts: statement list;
159
   hand_asserts: assert_t list;
160
   hand_annots: expr_annot list;
161
   hand_loc: Location.t}
162

  
163
type node_desc =
164
    {node_id: ident;
165
     mutable node_type: Types.type_expr;
166
     mutable node_clock: Clocks.clock_expr;
167
     node_inputs: var_decl list;
168
     node_outputs: var_decl list;
169
     node_locals: var_decl list;
170
     mutable node_gencalls: expr list;
171
     mutable node_checks: Dimension.dim_expr list;
172
     node_asserts: assert_t list;
173
     node_stmts: statement list;
174
     mutable node_dec_stateless: bool;
175
     mutable node_stateless: bool option;
176
     node_spec: node_annot option;
177
     node_annot: expr_annot list;
178
    }
179

  
180
type imported_node_desc =
181
    {nodei_id: ident;
182
     mutable nodei_type: Types.type_expr;
183
     mutable nodei_clock: Clocks.clock_expr;
184
     nodei_inputs: var_decl list;
185
     nodei_outputs: var_decl list;
186
     nodei_stateless: bool;
187
     nodei_spec: node_annot option;
188
     (* nodei_annot: expr_annot list; *)
189
     nodei_prototype: string option;
190
     nodei_in_lib: string list;
191
    }
192

  
193
type const_desc =
194
    {const_id: ident;
195
     const_loc: Location.t;
196
     const_value: constant;
197
     mutable const_type: Types.type_expr;
198
    }
199

  
200
type top_decl_desc =
201
| Node of node_desc
202
| Const of const_desc
203
| ImportedNode of imported_node_desc
204
| Open of bool * string (* the boolean set to true denotes a local
205
			   lusi vs a lusi installed at system level *)
206
| TypeDef of typedef_desc
207

  
208
type top_decl =
209
    {top_decl_desc: top_decl_desc;      (* description of the symbol *)
210
     top_decl_owner: Location.filename; (* the module where it is defined *)
211
     top_decl_itf: bool;                (* header or source file ? *)
212
     top_decl_loc: Location.t}          (* the location where it is defined *)
213

  
214
type program = top_decl list
215

  
216
type dep_t = Dep of
217
    bool
218
  * ident
219
  * (top_decl list)
220
  * bool (* is stateful *)
221

  
222

  
223
(************ Machine code types *************)
224

  
225
type value_t =
226
  {
227
    value_desc: value_t_desc;
228
    value_type: Types.type_expr;
229
    value_annot: expr_annot option
230
  }
231
and value_t_desc =
232
  | Cst of constant
233
  | LocalVar of var_decl
234
  | StateVar of var_decl
235
  | Fun of ident * value_t list
236
  | Array of value_t list
237
  | Access of value_t * value_t
238
  | Power of value_t * value_t
239

  
240
type instr_t =
241
  {
242
    instr_desc: instr_t_desc; (* main data: the content *)
243
    (* lustre_expr: expr option; (* possible representation as a lustre expression *) *)
244
    lustre_eq: eq option;     (* possible representation as a lustre flow equation *)
245
  }
246
and instr_t_desc =
247
  | MLocalAssign of var_decl * value_t
248
  | MStateAssign of var_decl * value_t
249
  | MReset of ident
250
  | MNoReset of ident
251
  | MStep of var_decl list * ident * value_t list
252
  | MBranch of value_t * (label * instr_t list) list
253
  | MComment of string
254

  
255

  
256
(* Local Variables: *)
257
(* compile-command:"make -C .." *)
258
(* End: *)
src/lustre_types.ml
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
type ident = Utils.ident
13
type rat = Utils.rat
14
type tag = Utils.tag
15
type label = Utils.ident
16

  
17
type type_dec =
18
    {ty_dec_desc: type_dec_desc;
19
     ty_dec_loc: Location.t}
20

  
21
and type_dec_desc =
22
  | Tydec_any
23
  | Tydec_int
24
  | Tydec_real
25
  (* | Tydec_float *)
26
  | Tydec_bool
27
  | Tydec_clock of type_dec_desc
28
  | Tydec_const of ident
29
  | Tydec_enum of ident list
30
  | Tydec_struct of (ident * type_dec_desc) list
31
  | Tydec_array of Dimension.dim_expr * type_dec_desc
32

  
33
type typedec_desc =
34
    {tydec_id: ident}
35

  
36
type typedef_desc =
37
    {tydef_id: ident;
38
     tydef_desc: type_dec_desc}
39

  
40
type clock_dec =
41
    {ck_dec_desc: clock_dec_desc;
42
     ck_dec_loc: Location.t}
43

  
44
and clock_dec_desc =
45
  | Ckdec_any
46
  | Ckdec_bool of (ident * ident) list
47

  
48

  
49
type constant =
50
  | Const_int of int
51
  | Const_real of Num.num * int * string (* (a, b, c) means a * 10^-b. c is the original string *)
52
  | Const_array of constant list
53
  | Const_tag of label
54
  | Const_string of string (* used only for annotations *)
55
  | Const_struct of (label * constant) list
56

  
57
type quantifier_type = Exists | Forall
58

  
59
type var_decl =
60
    {var_id: ident;
61
     var_orig:bool;
62
     var_dec_type: type_dec;
63
     var_dec_clock: clock_dec;
64
     var_dec_const: bool;
65
     var_dec_value: expr option;
66
     mutable var_parent_nodeid: ident option;
67
     mutable var_type: Types.type_expr;
68
     mutable var_clock: Clocks.clock_expr;
69
     var_loc: Location.t}
70

  
71
(** The core language and its ast. Every element of the ast contains its
72
    location in the program text. The type and clock of an ast element
73
    is mutable (and initialized to dummy values). This avoids to have to
74
    duplicate ast structures (e.g. ast, typed_ast, clocked_ast). *)
75

  
76

  
77

  
78
(* The tag of an expression is a unique identifier used to distinguish
79
   different instances of the same node *)
80
and expr =
81
    {expr_tag: tag;
82
     expr_desc: expr_desc;
83
     mutable expr_type: Types.type_expr;
84
     mutable expr_clock: Clocks.clock_expr;
85
     mutable expr_delay: Delay.delay_expr;
86
     mutable expr_annot: expr_annot option;
87
     expr_loc: Location.t}
88

  
89
and expr_desc =
90
  | Expr_const of constant
91
  | Expr_ident of ident
92
  | Expr_tuple of expr list
93
  | Expr_ite   of expr * expr * expr
94
  | Expr_arrow of expr * expr
95
  | Expr_fby of expr * expr
96
  | Expr_array of expr list
97
  | Expr_access of expr * Dimension.dim_expr
98
  | Expr_power of expr * Dimension.dim_expr
99
  | Expr_pre of expr
100
  | Expr_when of expr * ident * label
101
  | Expr_merge of ident * (label * expr) list
102
  | Expr_appl of call_t
103

  
104
and call_t = ident * expr * expr option
105
     (* The third part denotes the boolean condition for resetting *)
106

  
107
and eq =
108
    {eq_lhs: ident list;
109
     eq_rhs: expr;
110
     eq_loc: Location.t}
111

  
112
  (* The tag of an expression is a unique identifier used to distinguish
113
     different instances of the same node *)
114
and  eexpr =
115
    {eexpr_tag: tag;
116
     eexpr_qfexpr: expr;
117
     eexpr_quantifiers: (quantifier_type * var_decl list) list;
118
     mutable eexpr_type: Types.type_expr;
119
     mutable eexpr_clock: Clocks.clock_expr;
120
     mutable eexpr_normalized: (var_decl * eq list * var_decl list) option;
121
     eexpr_loc: Location.t}
122

  
123
and expr_annot =
124
 {annots: (string list * eexpr) list;
125
  annot_loc: Location.t}
126

  
127
type node_annot = {
128
  requires: eexpr list;
129
  ensures: eexpr list;
130
  behaviors: (string * eexpr list * eexpr list * Location.t) list;
131
  spec_loc: Location.t;
132
}
133

  
134
type offset =
135
| Index of Dimension.dim_expr
136
| Field of label
137

  
138
type assert_t =
139
    {
140
      assert_expr: expr;
141
      assert_loc: Location.t;
142
    }
143

  
144
type statement =
145
| Eq of eq
146
| Aut of automata_desc
147

  
148
and automata_desc =
149
  {aut_id : ident;
150
   aut_handlers: handler_desc list;
151
   aut_loc: Location.t}
152

  
153
and handler_desc =
154
  {hand_state: ident;
155
   hand_unless: (Location.t * expr * bool * ident) list;
156
   hand_until: (Location.t * expr * bool * ident) list;
157
   hand_locals: var_decl list;
158
   hand_stmts: statement list;
159
   hand_asserts: assert_t list;
160
   hand_annots: expr_annot list;
161
   hand_loc: Location.t}
162

  
163
type node_desc =
164
    {node_id: ident;
165
     mutable node_type: Types.type_expr;
166
     mutable node_clock: Clocks.clock_expr;
167
     node_inputs: var_decl list;
168
     node_outputs: var_decl list;
169
     node_locals: var_decl list;
170
     mutable node_gencalls: expr list;
171
     mutable node_checks: Dimension.dim_expr list;
172
     node_asserts: assert_t list;
173
     node_stmts: statement list;
174
     mutable node_dec_stateless: bool;
175
     mutable node_stateless: bool option;
176
     node_spec: node_annot option;
177
     node_annot: expr_annot list;
178
    }
179

  
180
type imported_node_desc =
181
    {nodei_id: ident;
182
     mutable nodei_type: Types.type_expr;
183
     mutable nodei_clock: Clocks.clock_expr;
184
     nodei_inputs: var_decl list;
185
     nodei_outputs: var_decl list;
186
     nodei_stateless: bool;
187
     nodei_spec: node_annot option;
188
     (* nodei_annot: expr_annot list; *)
189
     nodei_prototype: string option;
190
     nodei_in_lib: string list;
191
    }
192

  
193
type const_desc =
194
    {const_id: ident;
195
     const_loc: Location.t;
196
     const_value: constant;
197
     mutable const_type: Types.type_expr;
198
    }
199

  
200
type top_decl_desc =
201
| Node of node_desc
202
| Const of const_desc
203
| ImportedNode of imported_node_desc
204
| Open of bool * string (* the boolean set to true denotes a local
205
			   lusi vs a lusi installed at system level *)
206
| TypeDef of typedef_desc
207

  
208
type top_decl =
209
    {top_decl_desc: top_decl_desc;      (* description of the symbol *)
210
     top_decl_owner: Location.filename; (* the module where it is defined *)
211
     top_decl_itf: bool;                (* header or source file ? *)
212
     top_decl_loc: Location.t}          (* the location where it is defined *)
213

  
214
type program = top_decl list
215

  
216
type dep_t = Dep of
217
    bool
218
  * ident
219
  * (top_decl list)
220
  * bool (* is stateful *)
221

  
222

  
223

  
224

  
225
(* Local Variables: *)
226
(* compile-command:"make -C .." *)
227
(* End: *)
src/machine_code.ml
9 9
(*                                                                  *)
10 10
(********************************************************************)
11 11

  
12
open LustreSpec
12
open Lustre_types
13
open Machine_code_types
13 14
open Corelang
14 15
open Clocks
15 16
open Causality
......
213 214
    top_decl_loc = Location.dummy_loc
214 215
  }
215 216

  
216
let mk_val v t = { value_desc = v; 
217
		   value_type = t; 
218
		   value_annot = None }
219

  
217
let mk_val v t =
218
  { value_desc = v; 
219
    value_type = t; 
220
    value_annot = None }
221
    
220 222
let arrow_machine =
221 223
  let state = "_first" in
222 224
  let var_state = dummy_var_decl state Type_predef.type_bool(* (Types.new_ty Types.Tbool) *) in
src/machine_code_types.ml
1
(************ Machine code types *************)
2
open Lustre_types
3
  
4
type value_t =
5
  {
6
    value_desc: value_t_desc;
7
    value_type: Types.type_expr;
8
    value_annot: expr_annot option
9
  }
10
and value_t_desc =
11
  | Cst of constant
12
  | LocalVar of var_decl
13
  | StateVar of var_decl
14
  | Fun of ident * value_t list
15
  | Array of value_t list
16
  | Access of value_t * value_t
17
  | Power of value_t * value_t
18

  
19
type instr_t =
20
  {
21
    instr_desc: instr_t_desc; (* main data: the content *)
22
    (* lustre_expr: expr option; (* possible representation as a lustre expression *) *)
23
    lustre_eq: eq option;     (* possible representation as a lustre flow equation *)
24
  }
25
and instr_t_desc =
26
  | MLocalAssign of var_decl * value_t
27
  | MStateAssign of var_decl * value_t
28
  | MReset of ident
29
  | MNoReset of ident
30
  | MStep of var_decl list * ident * value_t list
31
  | MBranch of value_t * (label * instr_t list) list
32
  | MComment of string
src/main_lustre_compiler.ml
14 14
open Compiler_common
15 15

  
16 16
open Utils
17
open LustreSpec
17
open Lustre_types
18 18
 
19 19

  
20 20
let usage = "Usage: lustrec [options] \x1b[4msource file\x1b[0m"
src/main_lustre_testgen.ml
15 15
open Log
16 16

  
17 17
open Utils
18
open LustreSpec
18
open Lustre_types
19 19
open Compiler_common
20 20

  
21 21
let usage = "Usage: lustret [options] \x1b[4msource file\x1b[0m"
src/modules.ml
10 10
(********************************************************************)
11 11

  
12 12
open Utils
13
open LustreSpec
13
open Lustre_types
14 14
open Corelang
15 15

  
16 16
let add_symbol loc msg hashtbl name value =
src/mpfr.ml
10 10
(********************************************************************)
11 11

  
12 12
open Utils
13
open LustreSpec
13
open Lustre_types
14
open Machine_code_types
14 15
open Corelang
15 16
open Normalization
16 17
open Machine_code
src/mutation.ml
10 10
*)
11 11

  
12 12

  
13
open LustreSpec
13
open Lustre_types
14 14
open Corelang
15 15
open Log
16 16
open Format
src/normalization.ml
10 10
(********************************************************************)
11 11

  
12 12
open Utils
13
open LustreSpec
13
open Lustre_types
14 14
open Corelang
15 15
open Format
16 16

  
src/optimize_machine.ml
10 10
(********************************************************************)
11 11

  
12 12
open Utils
13
open LustreSpec 
13
open Lustre_types 
14
open Machine_code_types
14 15
open Corelang
15 16
open Causality
16 17
open Machine_code 
src/parse.ml
9 9
(*                                                                  *)
10 10
(********************************************************************)
11 11
open Format
12
open LustreSpec
12
open Lustre_types
13 13
open Corelang
14 14

  
15 15
type error =
src/parser_lustre.mly
11 11

  
12 12
%{
13 13
open Utils
14
open LustreSpec
14
open Lustre_types
15 15
open Corelang
16 16
open Dimension
17 17
open Parse
......
61 61
%token <string> IDENT
62 62
%token <string> UIDENT
63 63
%token TRUE FALSE
64
%token <LustreSpec.expr_annot> ANNOT
65
%token <LustreSpec.node_annot> NODESPEC
64
%token <Lustre_types.expr_annot> ANNOT
65
%token <Lustre_types.node_annot> NODESPEC
66 66
%token LBRACKET RBRACKET LCUR RCUR LPAR RPAR SCOL COL COMMA COLCOL 
67 67
%token AMPERAMPER BARBAR NOT POWER
68 68
%token IF THEN ELSE
......
106 106
%nonassoc LBRACKET
107 107

  
108 108
%start prog
109
%type <LustreSpec.top_decl list> prog
109
%type <Lustre_types.top_decl list> prog
110 110

  
111 111
%start header
112
%type <LustreSpec.top_decl list> header
112
%type <Lustre_types.top_decl list> header
113 113

  
114 114
%start lustre_annot
115
%type <LustreSpec.expr_annot> lustre_annot
115
%type <Lustre_types.expr_annot> lustre_annot
116 116

  
117 117
%start lustre_spec
118
%type <LustreSpec.node_annot> lustre_spec
118
%type <Lustre_types.node_annot> lustre_spec
119 119

  
120 120
%start signed_const
121
%type <LustreSpec.constant> signed_const
121
%type <Lustre_types.constant> signed_const
122 122

  
123 123
%start expr
124
%type <LustreSpec.expr> expr
124
%type <Lustre_types.expr> expr
125 125

  
126 126
%start stmt_list
127
%type <LustreSpec.statement list * LustreSpec.assert_t list * LustreSpec.expr_annot list > stmt_list
127
%type <Lustre_types.statement list * Lustre_types.assert_t list * Lustre_types.expr_annot list > stmt_list
128 128

  
129 129
%start vdecl_list
130
%type <LustreSpec.var_decl list> vdecl_list
130
%type <Lustre_types.var_decl list> vdecl_list
131 131
%%
132 132

  
133 133
module_ident:
src/pathConditions.ml
1
open LustreSpec 
1
open Lustre_types 
2 2
open Corelang
3 3
open Log
4 4
open Format
......
91 91
  (*   Printers.pp_expr expr (\*v*\) *)
92 92
  (*   Printers.pp_expr expr_neg_vi) *)
93 93
    
94
let rec compute_neg_expr cpt_pre (expr: LustreSpec.expr) =
94
let rec compute_neg_expr cpt_pre (expr: Lustre_types.expr) =
95 95
  let neg_list l = 
96 96
    List.fold_right (fun e (vl,el) -> let vl', e' = compute_neg_expr cpt_pre e in (vl'@vl), e'::el) l ([], [])
97 97
  in
src/pluginType.ml
4 4
  val activate: unit -> unit
5 5
  val options: (string * Arg.spec * string) list
6 6
  val check_force_stateful : unit -> bool
7
  val refine_machine_code: LustreSpec.top_decl list ->
7
  val refine_machine_code: Lustre_types.top_decl list ->
8 8
    Machine_code.machine_t list -> Machine_code.machine_t list
9 9
  val c_backend_main_loop_body_prefix : string -> string -> Format.formatter ->  unit -> unit
10 10
  val c_backend_main_loop_body_suffix : Format.formatter ->  unit -> unit
src/plugins.ml
1
open LustreSpec
1
open Lustre_types
2 2

  
3 3
open PluginList
4 4

  
src/plugins/salsa/machine_salsa_opt.ml
2 2
(* We try to avoid opening modules here *)
3 3
module ST = Salsa.Types
4 4
module SDT = SalsaDatatypes
5
module LT = LustreSpec
5
module LT = Lustre_types
6 6
module MC = Machine_code
7 7

  
8 8
(* Datatype for Salsa: FormalEnv, Ranges, Var set ... *)
......
29 29
(******************************************************************)    
30 30

  
31 31
(* Returns the set of vars that appear in the expression *)
32
let rec get_expr_real_vars e = 
33
  match e.LT.value_desc with
34
  | LT.LocalVar v | LT.StateVar v when Types.is_real_type v.LT.var_type -> Vars.singleton v
35
  | LT.LocalVar _| LT.StateVar _
36
  | LT.Cst _ -> Vars.empty 
37
  | LT.Fun (_, args) -> 
32
let rec get_expr_real_vars e =
33
  let open MT in 
34
  match e.value_desc with
35
  | LocalVar v | StateVar v when Types.is_real_type v.LT.var_type -> Vars.singleton v
36
  | LocalVar _| StateVar _
37
  | Cst _ -> Vars.empty 
38
  | Fun (_, args) -> 
38 39
    List.fold_left 
39 40
      (fun acc e -> Vars.union acc (get_expr_real_vars e)) 
40 41
      Vars.empty args
41
  | LT.Array _
42
  | LT.Access _
43
  | LT.Power _ -> assert false 
42
  | Array _
43
  | Access _
44
  | Power _ -> assert false 
44 45

  
45 46
(* Extract the variables to appear as free variables in expressions (lhs) *)
46 47
let rec get_read_vars instrs =
48
  let open MT in
47 49
  match instrs with
48 50
    [] -> Vars.empty
49 51
  | i::tl -> (
50 52
    let vars_tl = get_read_vars tl in 
51 53
    match Corelang.get_instr_desc i with
52
    | LT.MLocalAssign(_,e) 
53
    | LT.MStateAssign(_,e) -> Vars.union (get_expr_real_vars e) vars_tl
54
    | LT.MStep(_, _, el) -> List.fold_left (fun accu e -> Vars.union (get_expr_real_vars e) accu) vars_tl el
55
    | LT.MBranch(e, branches) -> (
54
    | MLocalAssign(_,e) 
55
    | MStateAssign(_,e) -> Vars.union (get_expr_real_vars e) vars_tl
56
    | MStep(_, _, el) -> List.fold_left (fun accu e -> Vars.union (get_expr_real_vars e) accu) vars_tl el
57
    | MBranch(e, branches) -> (
56 58
      let vars = Vars.union (get_expr_real_vars e) vars_tl in
57 59
      List.fold_left (fun vars (_, b) -> Vars.union vars (get_read_vars b) ) vars branches
58 60
    )
59
    | LT.MReset _ 
60
    | LT.MNoReset _ 
61
    | LT.MComment _ -> Vars.empty  
61
    | MReset _ 
62
    | MNoReset _ 
63
    | MComment _ -> Vars.empty  
62 64
  )
63 65

  
64 66
let rec get_written_vars instrs =
67
  let open MT in
65 68
  match instrs with
66 69
    [] -> Vars.empty
67 70
  | i::tl -> (
68 71
    let vars_tl = get_written_vars tl in 
69 72
    match Corelang.get_instr_desc i with
70
    | LT.MLocalAssign(v,_) 
71
    | LT.MStateAssign(v,_) -> Vars.add v vars_tl 
72
    | LT.MStep(vdl, _, _) -> List.fold_left (fun accu v -> Vars.add v accu) vars_tl vdl
73
    | LT.MBranch(_, branches) -> (
73
    | MLocalAssign(v,_) 
74
    | MStateAssign(v,_) -> Vars.add v vars_tl 
75
    | MStep(vdl, _, _) -> List.fold_left (fun accu v -> Vars.add v accu) vars_tl vdl
76
    | MBranch(_, branches) -> (
74 77
      List.fold_left (fun vars (_, b) -> Vars.union vars (get_written_vars b) ) vars_tl branches
75 78
    )
76
    | LT.MReset _ 
77
    | LT.MNoReset _ 
78
    | LT.MComment _ -> Vars.empty    
79
    | MReset _ 
80
    | MNoReset _ 
81
    | MComment _ -> Vars.empty    
79 82
  )
80 83

  
81 84

  
82 85
(* Optimize a given expression. It returns another expression and a computed range. *)
83
let optimize_expr nodename m constEnv printed_vars vars_env ranges formalEnv e : LT.value_t * RangesInt.t option = 
86
let optimize_expr nodename m constEnv printed_vars vars_env ranges formalEnv e : MT.value_t * RangesInt.t option = 
84 87
  let rec opt_expr ranges formalEnv e =
85
    match e.LT.value_desc with
86
    | LT.Cst cst ->
88
    let open MT in
89
    match e.value_desc with
90
    | Cst cst ->
87 91
      (* Format.eprintf "optmizing constant expr @ "; *)
88 92
      (* the expression is a constant, we optimize it directly if it is a real
89 93
  	 constant *)
......
91 95
      if Types.is_real_type typ then 
92 96
	opt_num_expr ranges formalEnv e 
93 97
      else e, None
94
    | LT.LocalVar v
95
    | LT.StateVar v -> 
98
    | LocalVar v
99
    | StateVar v -> 
96 100
      if not (Vars.mem v printed_vars) && 
97 101
	(* TODO xAvier: comment recuperer le type de l'expression? Parfois e.value_type vaut 'd *)
98
	(Types.is_real_type e.LT.value_type ||  Types.is_real_type v.LT.var_type) 
102
	(Types.is_real_type e.value_type ||  Types.is_real_type v.LT.var_type) 
99 103
      then
100 104
	opt_num_expr ranges formalEnv e 
101 105
      else 
......
103 107
    (* (\* optimize only numerical vars *\) *)
104 108
    (* if Type_predef.is_real_type v.LT.var_type then opt_num_expr ranges formalEnv e *)
105 109
    (* else e, None *)
106
    | LT.Fun (fun_id, args) -> (
110
    | Fun (fun_id, args) -> (
107 111
      (* necessarily, this is a basic function (ie. + - * / && || mod ... ) *)
108 112
      (* if the return type is real then optimize it, otherwise call recusrsively on arguments *)
109
      if Types.is_real_type e.LT.value_type then
113
      if Types.is_real_type e.value_type then
110 114
	opt_num_expr ranges formalEnv e 
111 115
      else (
112 116
	(* We do not care for computed local ranges. *)
113 117
  	let args' = List.map (fun arg -> let arg', _ = opt_expr ranges formalEnv arg in arg') args in
114
  	{ e with LT.value_desc = LT.Fun(fun_id, args')}, None	  
118
  	{ e with value_desc = Fun(fun_id, args')}, None	  
115 119
      )
116 120
    )
117
    | LT.Array _
118
    | LT.Access _
119
    | LT.Power _ -> assert false  
121
    | Array _
122
    | Access _
123
    | Power _ -> assert false  
120 124
  and opt_num_expr ranges formalEnv e = 
121 125
     (* if !debug then Format.eprintf "Optimizing expression %a with Salsa@ " MC.pp_val e;  *)
122 126
    let fresh_id = "toto"  in (* TODO more meaningful name *)
......
237 241
	let e, r = optimize_expr nodename m constEnv printed_vars vars_env ranges formalEnv v_def in
238 242
	let instr_desc = 
239 243
	  if try (get_var vars_env v.LT.var_id).is_local with Not_found -> assert false then
240
	    LT.MLocalAssign(v, e)
244
	    MT.MLocalAssign(v, e)
241 245
	  else
242
	    LT.MStateAssign(v, e)
246
	    MT.MStateAssign(v, e)
243 247
	in
244 248
	(Corelang.mkinstr instr_desc)::accu_instr, 
245 249
	(match r with 
......
283 287
       Format.eprintf "Hdlist@.";
284 288
       let hd_instrs, ranges, formalEnv, printed_vars, vars_to_print =
285 289
	 match Corelang.get_instr_desc hd_instr with 
286
	 | LT.MLocalAssign(vd,vt) when Types.is_real_type vd.LT.var_type  && not (Vars.mem vd vars_to_print) -> 
290
	 | MT.MLocalAssign(vd,vt) when Types.is_real_type vd.LT.var_type  && not (Vars.mem vd vars_to_print) -> 
287 291
       Format.eprintf "local assign@.";
288 292
	    (* LocalAssign are injected into formalEnv *)
289 293
	    (* if !debug then Format.eprintf "Registering local assign %a@ " MC.pp_instr hd_instr; *)
......
295 299
	    printed_vars,              (* no new printed vars *)
296 300
	    vars_to_print              (* no more or less variables to print *)
297 301
	      
298
	 | LT.MLocalAssign(vd,vt) when Types.is_real_type vd.LT.var_type && Vars.mem vd vars_to_print ->
302
	 | MT.MLocalAssign(vd,vt) when Types.is_real_type vd.LT.var_type && Vars.mem vd vars_to_print ->
299 303
       Format.eprintf "local assign 2@.";
300 304

  
301 305
            (* if !debug then Format.eprintf "Registering and producing state assign %a@ " MC.pp_instr hd_instr; *)
......
314 318
	    Vars.add vd printed_vars,        (* adding vd to new printed vars *)
315 319
	    Vars.remove vd vars_to_print     (* removed vd from variables to print *)
316 320

  
317
	 | LT.MStateAssign(vd,vt) when Types.is_real_type vd.LT.var_type (* && Vars.mem vd vars_to_print  *)-> 
... This diff was truncated because it exceeds the maximum size that can be displayed.

Also available in: Unified diff