Source file parseTree.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
(* -------------------------------------------------------------------- *)
open Ident
open Location

(* -------------------------------------------------------------------- *)

let pp_lident fmt i = Format.fprintf fmt "%s" (unloc i)

type lident = ident loced
[@@deriving yojson, show {with_path = false}]

(* -------------------------------------------------------------------- *)
and container =
  | Aggregate
  | Partition
  | View

and type_r =
  | Tref       of lident
  | Tcontainer of type_t * container
  | Ttuple     of type_t list
  | Toption    of type_t
  | Tset       of type_t
  | Tlist      of type_t
  | Tmap       of type_t * type_t
  | Tcontract  of type_t
  | Tkeyof     of type_t

and type_t = type_r loced

(* -------------------------------------------------------------------- *)
and logical_operator =
  | And
  | Or
  | Xor
  | Imply
  | Equiv

and comparison_operator =
  | Equal
  | Nequal
  | Gt
  | Ge
  | Lt
  | Le

and arithmetic_operator =
  | Plus
  | Minus
  | Mult
  | DivRat
  | DivEuc
  | Modulo

and unary_operator =
  | Uminus
  | Not

and assignment_operator =
  | ValueAssign
  | PlusAssign
  | MinusAssign
  | MultAssign
  | DivAssign
  | AndAssign
  | OrAssign

and quantifier =
  | Forall
  | Exists

and operator =
  | Logical of logical_operator
  | Cmp     of comparison_operator
  | Arith   of arithmetic_operator
  | Unary   of unary_operator

type pattern_unloc =
  | Pwild
  | Pref of lident

and pattern = pattern_unloc loced

and var_label = VLBefore | VLIdent of lident

and var_vset  = VSAdded | VSUnmoved | VSRemoved

and for_ident_unloc = FIsimple of lident | FIdouble of lident * lident
and for_ident = for_ident_unloc loced

and transfer_t =
  | TTsimple   of expr
  | TTcontract of expr * lident * type_t * expr
  | TTentry    of lident * expr
  | TTself     of lident * expr list

and expr_unloc =
  | Eterm         of (var_vset option * var_label option) * lident
  | Eliteral      of literal
  | Earray        of expr list
  | Erecord       of record_item list
  | Etuple        of expr list
  | Edot          of expr * lident
  | Esqapp        of expr * expr
  | Emulticomp    of expr * (comparison_operator loced * expr) list
  | Eapp          of function_ * expr list
  | Emethod       of expr * lident * expr list
  | Etransfer     of expr * transfer_t
  | Edorequire    of expr * expr
  | Edofailif     of expr * expr
  | Efail         of expr
  | Eassign       of assignment_operator * expr * expr
  | Eif           of expr * expr * expr option
  | Efor          of lident option * for_ident * expr * expr
  | Eiter         of lident option * lident * expr option * expr * expr
  | Ewhile        of lident option * expr * expr
  | Eseq          of expr * expr
  | Eletin        of lident * type_t option * expr * expr * expr option
  | Evar          of lident * type_t option * expr
  | Ematchwith    of expr * branch list
  | Erecupdate    of expr * (lident * expr) list
  | Equantifier   of quantifier * lident * quantifier_kind * expr
  | Eassert       of lident
  | Elabel        of lident
  | Ereturn       of expr
  | Eoption       of option_
  | Eentrypoint   of type_t * expr * expr
  | Eunpack       of type_t * expr
  | Eself         of lident
  | Eany
  | Enothing
  | Einvalid

and branch = (pattern list * expr)

and scope =
  | Added
  | After
  | Before
  | Fixed
  | Removed
  | Stable

and quantifier_kind =
  | Qcollection of expr
  | Qtype of type_t

and option_ =
  | OSome of expr
  | ONone

and function_ =
  | Fident of lident
  | Foperator of operator loced

and literal =
  | Lint      of Core.big_int
  | Lnat      of Core.big_int
  | Ldecimal  of string
  | Ltz       of Core.big_int
  | Lmtz      of Core.big_int
  | Lutz      of Core.big_int
  | Laddress  of string
  | Lstring   of string
  | Lbool     of bool
  | Lduration of string
  | Ldate     of string
  | Lbytes    of string
  | Lpercent  of Core.big_int

and record_item = (assignment_operator * lident) option * expr

and expr = expr_unloc loced

and lident_typ = lident * type_t * extension list option

and label_expr = (lident * expr) loced

and label_exprs = label_expr list

(* -------------------------------------------------------------------- *)
and extension_unloc =
  | Eextension of lident * expr list (** extension *)

and extension = extension_unloc loced

and exts = extension list option

(* -------------------------------------------------------------------- *)
and field_unloc =
  | Ffield of lident * type_t * expr option * exts   (** field *)

and field = field_unloc loced

and args = lident_typ list

and invariants = (lident * expr list) list

and specification_item_unloc =
  | Vpredicate     of lident * args * expr
  | Vdefinition    of lident * type_t * lident * expr
  | Vvariable      of lident * type_t * expr option
  | Veffect        of expr
  | Vassert        of (lident * expr * invariants * lident list)
  | Vfails         of (lident * lident * type_t * expr) list
  | Vpostcondition of (lident * expr * invariants * lident list * postkind option)

and postkind = PKPost | PKInv

and specification_item = specification_item_unloc loced

and specification_unloc = specification_item list * exts

and specification = specification_unloc loced

and security_arg_unloc =
  | Sident of lident
  | Sdot   of lident * lident
  | Slist  of security_arg list
  | Sapp   of lident * security_arg list
  | Sbut   of lident * security_arg
  | Sto    of lident * security_arg

and security_arg = security_arg_unloc loced

and security_item_unloc = lident * lident * security_arg list

and security_item = security_item_unloc loced

and security_unloc = security_item list * exts

and security = security_unloc loced

and s_function = {
  name  : lident;
  args  : args;
  ret_t : type_t option;
  spec  : specification option;
  body  : expr;
  getter: bool;
}

and entry_properties = {
  accept_transfer : bool;
  calledby        : (expr * exts) option;
  require         : ((lident * expr * expr option) list * exts) option;
  failif          : ((lident * expr * expr option) list * exts) option;
  spec_fun        : specification option;
  functions       : (s_function loced) list;
}

and transition = (lident * (expr * exts) option * (expr * exts) option) list

(* -------------------------------------------------------------------- *)
and variable_kind =
  | VKvariable
  | VKconstant

and enum_kind =
  | EKenum of lident
  | EKstate

(* -------------------------------------------------------------------- *)
and declaration_unloc =
  | Darchetype     of lident * exts
  | Dvariable      of variable_decl
  | Denum          of enum_kind * enum_decl
  | Dasset         of asset_decl
  | Drecord        of record_decl
  | Dentry         of entry_decl
  | Dtransition    of transition_decl
  | Dextension     of extension_decl
  | Dnamespace     of namespace_decl
  | Dfunction      of s_function
  | Dspecification of specification
  | Dspecasset     of lident * label_exprs
  | Dspecfun       of bool * lident * args * specification (* true = entry *)
  | Dspecvariable  of lident * label_exprs
  | Dsecurity      of security
  | Dinvalid

and variable_decl =
  lident
  * type_t
  * expr option
  * variable_kind
  * label_exprs
  * exts

and enum_decl =
  (lident * enum_option list) list * exts

and asset_decl =
  lident
  * field list
  * field list (* shadow fields *)
  * asset_option list
  * asset_post_option list
  * asset_operation option
  * exts

and record_decl =
  lident
  * field list
  * exts

and entry_decl =
  lident
  * args
  * entry_properties
  * (expr * exts) option
  * exts

and transition_decl =
  lident
  * args
  * (lident * type_t) option
  * expr
  * entry_properties
  * transition
  * exts

and extension_decl =
  lident * expr list

and namespace_decl =
  lident * declaration list

and asset_option =
  | AOidentifiedby of lident list
  | AOsortedby of lident
  | AOto of lident

and asset_post_option =
  | APOstates of lident
  | APOconstraints of label_exprs
  | APOinit of expr list

and enum_option =
  | EOinitial
  | EOspecification of label_exprs

and declaration = declaration_unloc loced

and asset_operation_enum =
  | AOadd
  | AOremove
  | AOupdate

and asset_operation =
  | AssetOperation of asset_operation_enum list * expr option

(* -------------------------------------------------------------------- *)
and archetype_unloc =
  | Marchetype of declaration list
  | Mextension of lident * declaration list * declaration list

and archetype = archetype_unloc loced
[@@deriving yojson, show {with_path = false},
            visitors { variety = "map"; ancestors = ["location_map"; "ident_map"] },
            visitors { variety = "iter"; ancestors = ["location_iter"; "ident_iter"] },
            visitors { variety = "reduce"; ancestors = ["location_reduce"; "ident_reduce"] },
            visitors { variety = "reduce2"; ancestors = ["location_reduce2"; "ident_reduce2"] }
    ]

let mk_archetype ?(decls=[]) ?(loc=dummy) () =
  mkloc loc (Marchetype decls)

let is_keyword = function
  | "added"
  | "aggregate"
  | "and"
  | "any"
  | "archetype"
  | "assert"
  | "asset"
  | "at"
  | "before"
  | "but"
  | "by"
  | "call"
  | "called"
  | "constant"
  | "contract"
  | "definition"
  | "div"
  | "do"
  | "dofailif"
  | "done"
  | "dorequire"
  | "effect"
  | "else"
  | "end"
  | "entry"
  | "entrypoint"
  | "enum"
  | "exists"
  | "extension"
  | "fail"
  | "failif"
  | "fails"
  | "false"
  | "for"
  | "forall"
  | "from"
  | "function"
  | "getter"
  | "identified"
  | "if"
  | "in"
  | "initial"
  | "initialized"
  | "invariant"
  | "iter"
  | "label"
  | "let"
  | "list"
  | "map"
  | "match"
  | "namespace"
  | "none"
  | "not"
  | "on"
  | "option"
  | "or"
  | "otherwise"
  | "partition"
  | "pkey"
  | "postcondition"
  | "predicate"
  | "record"
  | "ref"
  | "removed"
  | "require"
  | "return"
  | "security"
  | "set"
  | "self"
  | "shadow"
  | "some"
  | "sorted"
  | "specification"
  | "states"
  | "then"
  | "to"
  | "transfer"
  | "transition"
  | "true"
  | "unmoved"
  | "unpack"
  | "use"
  | "var"
  | "view"
  | "variable"
  | "when"
  | "while"
  | "with"
  | "xor"
    -> true
  | _ -> false