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
|