Source file frontend.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
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
(**
Universal frontend translates the parser's AST into Framework's AST.
*)
open Mopsa
open Mopsa_universal_parser
module NameG =
struct
let compt = ref 0
let fresh () =
let rep = !compt in
incr compt;
rep
end
open Lexing
open Ast
open Mopsa
module T = Ast
module U = U_ast
module Float = ItvUtils.Float
module MS = MapExt.StringMap
type var_context = (int * typ) MS.t
type fun_context = (T.fundec) MS.t
let builtin_functions =
[
{name = "mopsa_assume"; args = [None]; output = T_unit};
{name = "append"; args = [Some (T_array T_int); Some T_int]; output = T_unit};
]
let from_extent (e: U.extent) : Location.range = e
type uvar = {
uvar_range: range;
uvar_uid: int;
uvar_orig_name: string;
uvar_uniq_name: string;
}
type var_kind +=
| V_uvar of uvar
let () = register_var {
print = (fun next fmt v ->
match vkind v with
| V_uvar var ->
if !Framework.Core.Ast.Var.print_uniq_with_uid then
Format.fprintf fmt "%s:%a" var.uvar_orig_name pp_relative_range var.uvar_range
else Format.fprintf fmt "%s" var.uvar_orig_name
| _ -> next fmt v
);
compare = (fun next v1 v2 ->
match vkind v1, vkind v2 with
| V_uvar var1, V_uvar var2 ->
Compare.compose [
(fun () -> Stdlib.compare var1.uvar_uid var2.uvar_uid);
(fun () -> Stdlib.compare var1.uvar_uniq_name var2.uvar_uniq_name)
]
| _ -> next v1 v2
);
}
let from_var (v: string) (ext: U.extent) (var_ctx: var_context) =
try
let (id, typ) = MS.find v var_ctx in
let uniq_name = (v ^ ":" ^ string_of_int id) in
mkv uniq_name
(V_uvar {
uvar_range = ext;
uvar_uid = id;
uvar_orig_name = v;
uvar_uniq_name = uniq_name
})
typ
with
| Not_found ->
Exceptions.panic_at ext
"%s was not found in typing/naming context"
v
let rec from_typ (typ: U_ast.typ) : typ =
match typ with
| AST_INT -> T_int
| AST_REAL -> T_float F_DOUBLE
| AST_ARRAY t -> T_array (from_typ t)
| AST_STRING -> T_string
| AST_CHAR -> T_char
let unify_typ (x:typ) (y:typ) : typ =
match x,y with
| T_int, T_float _ -> y
| T_float _, T_int -> x
| _ ->
if compare_typ x y = 0 then x
else Exceptions.panic "cannot unify types %a and %a" pp_typ x pp_typ y
let to_typ (t:typ) (e:expr) : expr =
let range = erange e in
let orgt = etyp e in
if compare_typ orgt t = 0 then e
else
match ekind e, orgt, t with
| _, (T_int | T_float _), (T_int | T_float _) ->
mk_unop O_cast e ~etyp:t range
| E_constant (C_top T_any), T_any, t ->
{e with ekind = E_constant (C_top t); etyp = t}
| _ ->
Exceptions.panic "cannot convert expression %a of type %a to type %a" pp_expr e pp_typ orgt pp_typ t
let from_binop (t: typ) (b: U.binary_op) : operator =
match t, b with
| T_int, AST_PLUS -> O_plus
| T_int, AST_MINUS -> O_minus
| T_int, AST_MULTIPLY -> O_mult
| T_int, AST_DIVIDE -> O_div
| T_int, AST_EQUAL -> O_eq
| T_int, AST_NOT_EQUAL -> O_ne
| T_int, AST_LESS -> O_lt
| T_int, AST_LESS_EQUAL -> O_le
| T_int, AST_GREATER -> O_gt
| T_int, AST_GREATER_EQUAL -> O_ge
| T_int, AST_AND -> O_log_and
| T_int, AST_OR -> O_log_or
| T_string, AST_CONCAT -> O_concat
| T_string, AST_PLUS -> O_concat
| T_string, AST_EQUAL -> O_eq
| T_float _, AST_PLUS -> O_plus
| T_float _, AST_MINUS -> O_minus
| T_float _, AST_MULTIPLY -> O_mult
| T_float _, AST_DIVIDE -> O_div
| T_float _, AST_EQUAL -> O_eq
| T_float _, AST_NOT_EQUAL -> O_ne
| T_float _, AST_LESS -> O_lt
| T_float _, AST_LESS_EQUAL -> O_le
| T_float _, AST_GREATER -> O_gt
| T_float _, AST_GREATER_EQUAL -> O_ge
| T_array _, AST_CONCAT -> O_concat
| _ -> Exceptions.panic "operator %a cannot be used with type %a" U_ast_printer.print_binary_op b pp_typ t
let from_unop (t: typ) (b: U.unary_op) : operator =
match t, b with
| T_int, AST_UNARY_PLUS -> O_plus
| T_int, AST_UNARY_MINUS -> O_minus
| T_int, AST_NOT -> O_log_not
| T_float f, AST_UNARY_PLUS -> O_plus
| T_float f, AST_UNARY_MINUS -> O_minus
| T_float f, AST_ROUND -> O_cast
| _ -> Exceptions.panic "operator %a cannot be used with type %a" U_ast_printer.print_unary_op b pp_typ t
let rec from_expr (e: U.expr) (ext : U.extent) (var_ctx: var_context) (fun_ctx: fun_context option): expr =
let range = from_extent ext in
match e with
| AST_unit_const -> mk_expr ~etyp:T_unit (E_constant (C_unit)) range
| AST_fun_call((f, f_ext), args) ->
begin
let look_in_builtins (fun_ctx) =
let exception Match of (expr list * fun_builtin) in
try
List.iter (fun (bi:fun_builtin) ->
let () = Debug.debug ~channel:("remove_me") "builtin: %s, fun: %s, b: %b" bi.name f (bi.name = f) in
if bi.name = f && List.length bi.args = List.length args then
let exception NoMatch in
try
let el = List.map2 (fun (e, ext) x ->
match x with
| Some x ->
let e' = from_expr e ext var_ctx (fun_ctx) in
let typ = etyp e' in
let () = Debug.debug ~channel:("remove_me") "x: %a, typ: %a" pp_typ x pp_typ typ in
if compare_typ typ x = 0 then
e'
else
raise NoMatch
| None -> from_expr e ext var_ctx (fun_ctx)
) args bi.args
in
raise (Match (el, bi))
with
| NoMatch -> ()
) builtin_functions;
Exceptions.panic_at ext
"%s was not found in naming context nor in builtin functions"
f
with
| Match(el, bi) ->
(mk_expr ~etyp:(bi.output) (E_call(mk_expr (E_function (Builtin bi)) range, el)) range)
in
match fun_ctx with
| None -> look_in_builtins (None)
| Some fun_ctx ->
begin
try
let fundec = MS.find f fun_ctx in
if List.length fundec.fun_parameters = List.length args then
let el = List.map2 (fun (e, ext) x ->
let e' = from_expr e ext var_ctx (Some fun_ctx) in
let typ = etyp e' in
if compare_typ x.vtyp typ = 0 then
e'
else
Exceptions.panic_at ext
"type of %a incompatible with declared function"
U_ast_printer.print_expr e
) args fundec.fun_parameters in
let rettyp =
match fundec.fun_return_type with
| None -> T_int
| Some t -> t
in
(mk_expr ~etyp:rettyp (E_call(mk_expr (E_function (User_defined fundec)) range, el)) range)
else
Exceptions.panic_at ext
"%s number of arguments incompatible with call"
f
with
| Not_found ->
begin
look_in_builtins (Some fun_ctx)
end
end
end
| AST_unary (op, (e, ext)) ->
begin
let e = from_expr e ext var_ctx fun_ctx in
let typ = etyp e in
let op = from_unop typ op in
mk_unop op e ~etyp:typ range
end
| AST_binary (op, (e1, ext1), (e2, ext2)) ->
begin
let e1 = from_expr e1 ext1 var_ctx fun_ctx in
let typ1 = etyp e1 in
let e2 = from_expr e2 ext2 var_ctx fun_ctx in
let typ2 = etyp e2 in
let typ = unify_typ typ1 typ2 in
let e1,e2 = to_typ typ e1, to_typ typ e2 in
let op = from_binop typ op in
mk_binop e1 op e2 ~etyp:typ range
end
| AST_identifier (v, ext) ->
mk_var (from_var v ext var_ctx) range
| AST_int_const (s, _) ->
mk_z (Z.of_string s) range
| AST_bool_const (b, _) ->
mk_int (if b then 1 else 0) range
| AST_real_const (s, _) ->
let lo = Float.of_string `DOUBLE `DOWN s
and up = Float.of_string `DOUBLE `UP s
in
mk_float_interval ~prec:F_DOUBLE lo up range
| AST_string_const (s, _) ->
mk_string s range
| AST_char_const(c, _) ->
mk_int ~typ:T_int (int_of_char c) range
| AST_array_const(a, _) ->
mk_expr (E_array (List.map (fun (e, ext) -> from_expr e ext var_ctx fun_ctx) (Array.to_list a))) range
| AST_rand((l, _), (u, _)) ->
mk_z_interval (Z.of_string l) (Z.of_string u) range
| AST_randf((l, _), (u, _)) ->
mk_float_interval (float_of_string l) (float_of_string u) range
| AST_rand_string ->
mk_top T_any range
| AST_array_access((e1, ext1), (e2, ext2)) ->
begin
let e1o = e1 in
let e1 = from_expr e1 ext1 var_ctx fun_ctx in
let e2 = from_expr e2 ext2 var_ctx fun_ctx in
let e2 = to_typ T_int e2 in
match etyp e1 with
| T_string -> mk_expr (E_subscript(e1, e2)) ~etyp:T_int range
| T_array t -> mk_expr (E_subscript(e1, e2)) ~etyp:t range
| _ -> Exceptions.panic_at ext
"%a is of type %a and can not be subscripted"
U_ast_printer.print_expr e1o
(pp_typ) (etyp e1)
end
| AST_len (e, ext) ->
begin
let e1 = from_expr e ext var_ctx fun_ctx in
match etyp e1 with
| T_string
| T_array _ -> mk_expr (E_len e1) ~etyp:T_int range
| _ -> Exceptions.panic_at ext "%a is of type %a and can not be lengthed"
U_ast_printer.print_expr e
(pp_typ) (etyp e1)
end
let rec from_stmt (s: U.stat) (ext: U.extent) (var_ctx: var_context) (fun_ctx: fun_context option): stmt =
let range = from_extent ext in
match s with
| AST_block l ->
mk_block (List.map (fun (x, ext) -> from_stmt x ext var_ctx fun_ctx) l) range
| AST_assign((e1, ext1), (e2, ext2)) ->
begin
let e1o = e1 in
match e1 with
| AST_array_access(_, _)
| AST_identifier _ ->
let e1 = from_expr e1 ext1 var_ctx fun_ctx in
let e2 = from_expr e2 ext2 var_ctx fun_ctx in
let e2 = to_typ (etyp e1) e2 in
mk_assign e1 e2 range
| _ ->
Exceptions.panic_at ext "%a not considered a left-value for now "
U_ast_printer.print_expr e1o
end
| AST_if((e1, ext_e1), (s1, ext_s1), Some (s2, ext_s2)) ->
let e1 = from_expr e1 ext_e1 var_ctx fun_ctx in
let s1 = from_stmt s1 ext_s1 var_ctx fun_ctx in
let s2 = from_stmt s2 ext_s2 var_ctx fun_ctx in
mk_if e1 s1 s2 range
| AST_if((e1, ext_e1), (s1, ext_s1), None) ->
let e1 = from_expr e1 ext_e1 var_ctx fun_ctx in
let s1 = from_stmt s1 ext_s1 var_ctx fun_ctx in
mk_if e1 s1 (mk_nop range) range
| AST_while((e1, ext_e1), (s1, ext_s1)) ->
let e1 = from_expr e1 ext_e1 var_ctx fun_ctx in
let s1 = from_stmt s1 ext_s1 var_ctx fun_ctx in
mk_while e1 s1 range
| AST_for((v1, ext_v1), (e1, ext_e1), (e2, ext_e2), (s1, ext_s1)) ->
let e1 = from_expr e1 ext_e1 var_ctx fun_ctx in
let e2 = from_expr e2 ext_e2 var_ctx fun_ctx in
let v = from_var v1 ext_v1 var_ctx in
let s1 = from_stmt s1 ext_s1 var_ctx fun_ctx in
mk_block
[
mk_assign
(mk_var v (tag_range range "var_init_for_variable"))
e1
(tag_range range "expr_init_for_variable");
mk_while
(mk_binop
(mk_var v (tag_range range "var_comp_for"))
O_le
e2
~etyp:(T_int)
(tag_range range "comp_for")
)
(mk_block (
[
s1;
mk_assign
(mk_var v (tag_range range "var_incr_for"))
(mk_binop
(mk_var v (tag_range range "var_incr_for"))
O_plus
(mk_z Z.one (tag_range range "one_for"))
~etyp:(T_int)
(tag_range range "incr_for")
)
(tag_range range "assign_for")
])
(tag_range range "body_for")
)
(tag_range range "total_for")
]
range
| AST_return (Some (e, ext)) ->
let e = from_expr e ext var_ctx fun_ctx in
{skind = S_return (Some e);
srange = range
}
| AST_return None ->
{skind = S_return None;
srange = range
}
| AST_break ->
{skind = S_break; srange = range}
| AST_continue ->
{skind = S_continue; srange = range}
| AST_assert (e, ext) ->
let e = from_expr e ext var_ctx fun_ctx in
mk_assert e range
| AST_assume (e, ext) ->
let e = from_expr e ext var_ctx fun_ctx in
mk_assume e range
| AST_print ->
mk_stmt S_print_state range
| AST_expr(e, ext) ->
let e' = from_expr e ext var_ctx fun_ctx in
mk_expr_stmt e' range
let rec check_declaration_list (dl : U.declaration U.ext list) =
match dl with
| p::q -> aux p q; check_declaration_list q
| [] -> ()
and aux (((((_,v),e),_),_) as p : U.declaration U.ext) (dl: U.declaration U.ext list) =
match dl with
| ((((_,v'),e'),_),_)::q when v = v' -> Exceptions.panic_at e "%s has already been declared at %a"
v'
pp_range e'
| p':: q -> aux p q
| [] -> ()
let var_ctx_of_declaration (dl : U_ast.declaration U.ext list) (var_ctx: var_context) =
let () = check_declaration_list dl in
let add_var var_ctx v t =
try
MS.add v (NameG.fresh (), t) var_ctx
with
| Not_found ->
MS.add v (NameG.fresh (), t) var_ctx
in
let var_ctx, gvars = List.fold_left (fun (var_ctx, gvars) ((((t, v), extv ), o), e) ->
let new_var_ctx = add_var var_ctx v (from_typ t) in
let vv = from_var v extv new_var_ctx in
(new_var_ctx, vv :: gvars)
) (var_ctx, []) dl in
var_ctx, gvars
let var_ctx_init_of_declaration (dl : U_ast.declaration U.ext list) (var_ctx: var_context) (fun_ctx: fun_context option) (nvar_ctx)=
let add_var var_ctx v t =
try
match nvar_ctx with
| Some nvar_ctx -> MS.add v (MS.find v nvar_ctx) var_ctx
| None -> MS.add v (NameG.fresh (), t) var_ctx
with
| Not_found ->
assert false
in
let var_ctx, init, gvars = List.fold_left (fun (var_ctx, init, gvars) ((((t, v), extv ), o), e) ->
let new_var_ctx = add_var var_ctx v (from_typ t) in
let vv = from_var v extv new_var_ctx in
let range = from_extent extv in
let stmt_add = mk_add
(mk_var vv (tag_range range "initializer_var"))
(tag_range range "initializer") in
let init = stmt_add :: init in
match o with
| Some (e, ext) ->
let e = from_expr e ext var_ctx fun_ctx in
let e = to_typ (from_typ t) e in
let range = from_extent ext in
let stmt_init =
mk_assign
(mk_var vv (tag_range range "initializer_var"))
e
(tag_range range "initializer")
in
(new_var_ctx, stmt_init :: init, vv :: gvars)
| None ->
(new_var_ctx, init, vv :: gvars)
) (var_ctx, [], []) dl in
var_ctx, List.rev init, gvars
let var_ctx_of_function (var_ctx: var_context) (fundec: U.fundec) =
let add_var var_ctx v t =
try
MS.add v (NameG.fresh (), t) var_ctx
with
| Not_found ->
MS.add v (NameG.fresh (), t) var_ctx
in
let var_ctx = List.fold_left (fun acc ((t, v), _) ->
add_var acc v (from_typ t)
) var_ctx fundec.parameters in
let var_ctx, _ =
var_ctx_of_declaration fundec.locvars var_ctx
in
var_ctx
let var_init_of_function (var_ctx: var_context) var_ctx_map (fun_ctx: fun_context) (fundec: U.fundec) =
let nvar_ctx = MS.find fundec.funname var_ctx_map in
let add_var var_ctx n_var_ctx v t =
try
MS.add v (MS.find v n_var_ctx) var_ctx
with
| Not_found ->
assert false
in
let var_ctx = List.fold_left (fun acc ((t, v), _) ->
add_var acc nvar_ctx v (from_typ t)
) var_ctx fundec.parameters in
let var_ctx, init, _ =
var_ctx_init_of_declaration fundec.locvars var_ctx (Some (fun_ctx)) (Some nvar_ctx)
in
var_ctx, init
let from_fundec (f: U.fundec) (var_ctx: var_context): T.fundec =
let typ = OptionExt.lift from_typ f.return_type in
{
fun_orig_name = f.funname;
fun_uniq_name = f.funname;
fun_range = from_extent f.range;
fun_parameters = List.map (fun ((_, v), ext) -> from_var v ext var_ctx) f.parameters;
fun_locvars = List.map (fun ((((_, v), _), _), ext) -> from_var v ext var_ctx) f.locvars;
fun_body = mk_nop (from_extent (snd f.body));
fun_return_type = typ;
fun_return_var = None;
}
let fun_ctx_of_global (fl: U_ast.fundec U.ext list) (var_ctx: var_context) =
List.fold_left (fun (acc, var_ctx_map) (fundec, _) ->
let var_ctx = var_ctx_of_function var_ctx fundec in
(MS.add fundec.funname (from_fundec fundec var_ctx) acc, MS.add fundec.funname var_ctx var_ctx_map)
) (MS.empty, MS.empty) fl
let add_body (fl: fun_context) (f: string) (b: stmt): unit =
try
let fundec = MS.find f fl in
fundec.fun_body <- b;
with
| Not_found -> Exceptions.panic "[Universal.frontend] should not happen"
let from_prog (p: U_ast.prog) : prog_kind =
let ext = snd (p.main) in
let var_ctx, init, gvars = var_ctx_init_of_declaration p.gvars MS.empty None None in
let fun_ctx, var_ctx_map = fun_ctx_of_global p.funs var_ctx in
List.iter (fun (fundec, ext) ->
let var_ctx, init = var_init_of_function var_ctx var_ctx_map fun_ctx fundec in
let body = from_stmt (fst fundec.body) (snd fundec.body) var_ctx (Some fun_ctx) in
let total = mk_block (init @ [body]) (from_extent ext) in
add_body fun_ctx fundec.funname total
) p.funs;
let total = from_stmt (fst p.main) (snd p.main) var_ctx (Some fun_ctx) in
let with_init = mk_block (init @ [total]) (from_extent ext) in
P_universal
{
universal_gvars = gvars;
universal_fundecs = (MS.bindings fun_ctx) |> List.map (snd);
universal_main = with_init
}
let rec parse_program (files: string list): program =
match files with
| [filename] ->
let ast = U_file_parser.parse_file filename in
{
prog_kind = from_prog ast;
prog_range = mk_program_range [filename];
}
| [] -> panic "no input file"
| _ -> panic "analysis of multiple files not supported"
let () =
register_frontend {
lang = "universal";
parse = parse_program;
on_panic = fun _ _ _ -> ();
}