Project

General

Profile

Download (6 KB) Statistics
| Branch: | Tag: | Revision:
1
open Utils
2

    
3
type label = ident
4

    
5
type type_dec = { ty_dec_desc : type_dec_desc; ty_dec_loc : Location.t }
6

    
7
and type_dec_desc =
8
  | Tydec_any
9
  | Tydec_int
10
  | Tydec_real
11
  (* | Tydec_float *)
12
  | Tydec_bool
13
  | Tydec_clock of type_dec_desc
14
  | Tydec_const of ident
15
  | Tydec_enum of ident list
16
  | Tydec_struct of (ident * type_dec_desc) list
17
  | Tydec_array of Dimension.t * type_dec_desc
18

    
19
type typedec_desc = { tydec_id : ident }
20

    
21
type typedef_desc = { tydef_id : ident; tydef_desc : type_dec_desc }
22

    
23
type clock_dec = { ck_dec_desc : clock_dec_desc; ck_dec_loc : Location.t }
24

    
25
and clock_dec_desc = Ckdec_any | Ckdec_bool of (ident * ident) list
26

    
27
type constant =
28
  | Const_int of int
29
  | Const_real of Real.t
30
  | Const_array of constant list
31
  | Const_tag of label
32
  | Const_string of string
33
  (* used only for annotations *)
34
  | Const_modeid of string
35
  (* used only for annotations *)
36
  | Const_struct of (label * constant) list
37

    
38
type quantifier_type = Exists | Forall
39

    
40
type var_decl = {
41
  var_id : ident;
42
  var_orig : bool;
43
  var_dec_type : type_dec;
44
  var_dec_clock : clock_dec;
45
  var_dec_const : bool;
46
  var_dec_value : expr option;
47
  mutable var_parent_nodeid : ident option;
48
  mutable var_type : Types.t;
49
  mutable var_clock : Clocks.t;
50
  var_loc : Location.t;
51
  var_is_contract: bool;
52
}
53
(* The tag of an expression is a unique identifier used to distinguish different
54
   instances of the same node *)
55

    
56
(** The core language and its ast. Every element of the ast contains its
57
    location in the program text. The type and clock of an ast element is
58
    mutable (and initialized to dummy values). This avoids to have to duplicate
59
    ast structures (e.g. ast, typed_ast, clocked_ast). *)
60

    
61
and expr = {
62
  expr_tag : tag;
63
  expr_desc : expr_desc;
64
  mutable expr_type : Types.t;
65
  mutable expr_clock : Clocks.t;
66
  mutable expr_delay : Delay.t;
67
  mutable expr_annot : expr_annot option;
68
  expr_loc : Location.t;
69
}
70

    
71
and expr_desc =
72
  | Expr_const of constant
73
  | Expr_ident of ident
74
  | Expr_tuple of expr list
75
  | Expr_ite of expr * expr * expr
76
  | Expr_arrow of expr * expr
77
  | Expr_fby of expr * expr
78
  | Expr_array of expr list
79
  | Expr_access of expr * Dimension.t
80
  | Expr_power of expr * Dimension.t
81
  | Expr_pre of expr
82
  | Expr_when of expr * ident * label
83
  | Expr_merge of ident * (label * expr) list
84
  | Expr_appl of call_t
85

    
86
and call_t = ident * expr * expr option
87
(* The third part denotes the boolean condition for resetting *)
88

    
89
and eq = { eq_lhs : ident list; eq_rhs : expr; eq_loc : Location.t }
90

    
91
(* The tag of an expression is a unique identifier used to distinguish different
92
   instances of the same node *)
93
and eexpr = {
94
  eexpr_tag : tag;
95
  eexpr_qfexpr : expr;
96
  eexpr_quantifiers : (quantifier_type * var_decl list) list;
97
  eexpr_name : string option;
98
  mutable eexpr_type : Types.t;
99
  mutable eexpr_clock : Clocks.t;
100
  (* mutable eexpr_normalized: (var_decl * eq list * var_decl list) option; *)
101
  eexpr_loc : Location.t;
102
}
103

    
104
and expr_annot = { annots : (string list * eexpr) list; annot_loc : Location.t }
105

    
106
type contract_mode = {
107
  mode_id : ident;
108
  require : eexpr list;
109
  ensure : eexpr list;
110
  mode_loc : Location.t;
111
}
112

    
113
type contract_import = {
114
  import_nodeid : ident;
115
  inputs : expr;
116
  outputs : expr;
117
  import_loc : Location.t;
118
}
119

    
120
type offset = Index of Dimension.t | Field of label
121

    
122
type assert_t = { assert_expr : expr; assert_loc : Location.t }
123

    
124
type statement = Eq of eq | Aut of automata_desc
125

    
126
and automata_desc = {
127
  aut_id : ident;
128
  aut_handlers : handler_desc list;
129
  aut_loc : Location.t;
130
}
131

    
132
and handler_desc = {
133
  hand_state : ident;
134
  hand_unless : (Location.t * expr * bool * ident) list;
135
  hand_until : (Location.t * expr * bool * ident) list;
136
  hand_locals : var_decl list;
137
  hand_stmts : statement list;
138
  hand_asserts : assert_t list;
139
  hand_annots : expr_annot list;
140
  hand_loc : Location.t;
141
}
142

    
143
type proof_annotation = Kinduction of int
144

    
145
type contract_desc = {
146
  consts : var_decl list;
147
  locals : var_decl list;
148
  stmts : statement list;
149
  assume : eexpr list;
150
  guarantees : eexpr list;
151
  modes : contract_mode list;
152
  imports : contract_import list;
153
  spec_loc : Location.t;
154
  proof : proof_annotation option
155
}
156

    
157
type 'a node_spec_t = Contract of 'a | NodeSpec of ident
158

    
159
type node_desc = {
160
  node_id : ident;
161
  mutable node_type : Types.t;
162
  mutable node_clock : Clocks.t;
163
  node_inputs : var_decl list;
164
  node_outputs : var_decl list;
165
  node_locals : var_decl list;
166
  mutable node_gencalls : expr list;
167
  mutable node_checks : Dimension.t list;
168
  node_asserts : assert_t list;
169
  node_stmts : statement list;
170
  mutable node_dec_stateless : bool;
171
  mutable node_stateless : bool option;
172
  node_spec : contract_desc node_spec_t option;
173
  node_annot : expr_annot list;
174
  node_iscontract : bool;
175
}
176

    
177
type imported_node_desc = {
178
  nodei_id : ident;
179
  mutable nodei_type : Types.t;
180
  mutable nodei_clock : Clocks.t;
181
  nodei_inputs : var_decl list;
182
  nodei_outputs : var_decl list;
183
  nodei_stateless : bool;
184
  nodei_spec : contract_desc node_spec_t option;
185
  (* nodei_annot: expr_annot list; *)
186
  nodei_prototype : string option;
187
  nodei_in_lib : string list;
188
  nodei_iscontract : bool;
189
}
190

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

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

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

    
220
type program_t = top_decl list
221

    
222
type dep_t = {
223
  local : bool;
224
  name : ident;
225
  content : program_t;
226
  is_stateful : bool;
227
}
228

    
229
type spec_types =
230
  | LocalContract of contract_desc
231
  | TopContract of top_decl list
232

    
233
val tag_true : label
234

    
235
val tag_false : label
(44-44/99)