Source file ast.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
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
(**
Abstract Syntax Tree for stub specification. Similar to the AST of
the parser, except for expressions, types and variables for which
MOPSA counterparts are used.
*)
open Mopsa
open Universal.Ast
open Format
(** Stub for a function *)
type stub_func = {
stub_func_name : string;
stub_func_body : section list;
stub_func_params : var list;
stub_func_locals : local with_range list;
stub_func_assigns : assigns with_range list;
stub_func_return_type : typ option;
stub_func_range : range;
}
(** Stub for a global directive *)
and stub_directive = {
stub_directive_body : section list;
stub_directive_locals : local with_range list;
stub_directive_assigns : assigns with_range list;
stub_directive_range : range;
}
(** {2 Stub sections} *)
(** ***************** *)
and section =
| S_case of case
| S_leaf of leaf
and leaf =
| S_local of local with_range
| S_assumes of assumes with_range
| S_requires of requires with_range
| S_assigns of assigns with_range
| S_ensures of ensures with_range
| S_free of free with_range
| S_message of message with_range
and case = {
case_label : string;
case_body : leaf list;
case_locals : local with_range list;
case_assigns : assigns with_range list;
case_range : range;
}
(** {2 Leaf sections} *)
(** ***************** *)
and requires = formula with_range
and ensures = formula with_range
and assumes = formula with_range
and local = {
lvar : var;
lval : local_value;
}
and local_value =
| L_new of resource
| L_call of expr (** function *) * expr list
and assigns = {
assign_target : expr;
assign_offset : interval list;
}
and free = expr
and message = {
message_kind: message_kind;
message_body: string;
}
and message_kind =
| WARN
| UNSOUND
and log_binop = Mopsa_c_stubs_parser.Cst.log_binop =
| AND
| OR
| IMPLIES
and set =
| S_interval of interval
| S_resource of resource
and interval = expr * expr
and resource = Mopsa_c_stubs_parser.Ast.resource
and builtin = Mopsa_c_stubs_parser.Ast.builtin
(** {2 Formulas} *)
(** ************ *)
and formula =
| F_expr of expr
| F_binop of log_binop * formula with_range * formula with_range
| F_not of formula with_range
| F_forall of var * set * formula with_range
| F_exists of var * set * formula with_range
| F_in of expr * set
| F_otherwise of formula with_range * expr
| F_if of formula with_range * formula with_range * formula with_range
let compare_assigns a1 a2 =
Compare.pair compare_expr (Compare.list (Compare.pair compare_expr compare_expr))
(a1.assign_target, a2.assign_offset) (a2.assign_target, a2.assign_offset)
let compare_resource = Mopsa_c_stubs_parser.Ast.compare_resource
let compare_set s1 s2 =
match s1, s2 with
| S_interval(a1, b1), S_interval(a2, b2) ->
Compare.compose [
(fun () -> compare_expr a1 a2);
(fun () -> compare_expr b1 b2);
]
| S_resource r1, S_resource r2 ->
compare_resource r1 r2
| _ ->
compare s1 s2
let rec compare_formula f1 f2 =
match f1.content, f2.content with
| F_expr e1, F_expr e2 -> compare_expr e1 e2
| F_binop(o1, f1, g1), F_binop(o2, f2, g2) ->
Compare.compose [
(fun () -> compare o1 o2);
(fun () -> compare_formula f1 f2);
(fun () -> compare_formula g1 g2);
]
| F_not f1, F_not f2 -> compare_formula f1 f2
| F_forall(v1,s1,f1), F_forall(v2,s2,f2) ->
Compare.compose [
(fun () -> compare_var v1 v2);
(fun () -> compare_set s1 s2);
(fun () -> compare_formula f1 f2);
]
| F_exists(v1,s1,f1), F_exists(v2,s2,f2) ->
Compare.compose [
(fun () -> compare_var v1 v2);
(fun () -> compare_set s1 s2);
(fun () -> compare_formula f1 f2);
]
| F_in(e1,s1), F_in(e2,s2) ->
Compare.compose [
(fun () -> compare_expr e1 e2);
(fun () -> compare_set s1 s2)
]
| x,y -> compare x y
(** {2 Expressions} *)
(** Quantifiers *)
type quant =
| FORALL
| EXISTS
type expr_kind +=
| E_stub_call of stub_func (** called stub *) * expr list (** arguments *)
(** Call to a stubbed function *)
| E_stub_return
(** Returned value of a stub *)
| E_stub_builtin_call of builtin * expr list
(** Call to a built-in function *)
| E_stub_attribute of expr * string
(** Access to an attribute of a resource *)
| E_stub_alloc of string (** resource *) * mode (** strong or weak *)
(** Allocate a resource and translate it into an address *)
| E_stub_resource_mem of expr * resource
(** Filter environments in which an instance is in a resource pool *)
| E_stub_primed of expr
(** Primed expressions denoting values in the post-state *)
| E_stub_quantified_formula of (quant * var * set) list (** Prefix containing the list of quantified variables *) *
expr (** Quantifier-free formula *)
(** Quantified formula in prenex normal form *)
| E_stub_otherwise of expr (** condition *) * expr option (** alarm *)
(** Conditions decorated with failure alarms. If the alarm is not present, the
default alarm A_stub_invalid_requirement is raised. *)
| E_stub_raise of string (** message *)
(** Raise an alarm *)
| E_stub_if of expr (** condition *) * expr (** then *) * expr (** else *)
(** Conditional stub expression *)
(** {2 Statements} *)
type stmt_kind +=
| S_stub_directive of stub_directive
(** A call to a stub directive, which are stub functions called at the
initialization of the analysis. Useful to initialize variables with stub
formulas.
*)
| S_stub_free of expr
(** Release a resource *)
| S_stub_requires of expr
(** Filter the current environments that verify a condition, and raise an
alarm if the condition may be violated. *)
| S_stub_prepare_all_assigns of assigns list
(** Prepare primed copies of assigned objects *)
| S_stub_assigns of assigns
(** Declare an assigned object *)
| S_stub_clean_all_assigns of assigns list
(** Clean the post-state of primed copies *)
(** {2 Heap addresses for resources} *)
(** ******************************** *)
type addr_kind +=
| A_stub_resource of string (** resource address *)
let () =
register_addr_kind {
print = (fun next fmt addr_kind ->
match addr_kind with
| A_stub_resource res -> Format.pp_print_string fmt res
| _ -> next fmt addr_kind
);
compare = (fun next ak1 ak2 ->
match ak1, ak2 with
| A_stub_resource res1, A_stub_resource res2 -> Stdlib.compare res1 res2
| _ -> next ak1 ak2
);
}
let () = Universal.Heap.Policies.register_mk_addr (fun default ak ->
match ak with
| A_stub_resource _ -> Universal.Heap.Policies.mk_addr_stack_range ak
| _ -> default ak)
(** {2 Utility functions} *)
(** ********************* *)
let mk_stub_call stub args range =
let t = match stub.stub_func_return_type with
| None -> T_any
| Some t -> t
in
mk_expr (E_stub_call (stub, args)) ~etyp:t range
let mk_stub_builtin_call builtin arg ~etyp range =
mk_expr (E_stub_builtin_call (builtin,arg)) ~etyp range
let mk_stub_resource_mem e res range =
mk_expr (E_stub_resource_mem (e, res)) ~etyp:T_bool range
let mk_stub_primed e range =
mk_expr (E_stub_primed e) ~etyp:e.etyp range
let mk_stub_directive stub range =
mk_stmt (S_stub_directive stub) range
let mk_stub_free e range =
mk_stmt (S_stub_free e) range
let mk_stub_prepare_all_assigns assigns range =
mk_stmt (S_stub_prepare_all_assigns (List.map get_content assigns)) range
let mk_stub_assigns t offset range =
mk_stmt (S_stub_assigns { assign_target = t; assign_offset = offset}) range
let mk_stub_clean_all_assigns assigns range =
mk_stmt (S_stub_clean_all_assigns (List.map get_content assigns)) range
let mk_stub_requires cond range =
mk_stmt (S_stub_requires cond) range
let mk_stub_quantified_formula ?(etyp=T_bool) quants cond range =
mk_expr (E_stub_quantified_formula (quants, cond)) ~etyp range
let mk_stub_otherwise cond alarm ?(etyp=T_bool) range =
mk_expr (E_stub_otherwise (cond, alarm)) range ~etyp
let mk_stub_if c f1 f2 range =
mk_expr (E_stub_if (c, f1, f2)) range ~etyp:f1.etyp
let is_stub_primed e =
fold_expr
(fun acc ee ->
match ekind ee with
| E_stub_primed _ -> Keep true
| _ -> VisitParts acc
)
(fun acc stmt -> VisitParts acc)
false e
let find_var_quantifier v quants =
let rec iter = function
| [] -> raise Not_found
| (q,vv,s)::tl -> if compare_var v vv = 0 then (q,s) else iter tl
in
iter quants
let find_var_quantifier_opt v quants =
try Some (find_var_quantifier v quants)
with Not_found -> None
let is_quantified_var v quants =
match find_var_quantifier_opt v quants with
| None -> false
| Some _ -> true
let is_forall_quantified_var v quants =
match find_var_quantifier_opt v quants with
| None -> false
| Some (q,_) -> q = FORALL
let is_exists_quantified_var v quants =
match find_var_quantifier_opt v quants with
| None -> false
| Some (q,_) -> q = EXISTS
let find_quantified_var_interval v quants =
match find_var_quantifier v quants with
| (_,S_interval(lo,hi)) -> (lo,hi)
| _ -> raise Not_found
let find_quantified_var_interval_opt v quants =
try Some (find_quantified_var_interval v quants)
with Not_found -> None
let negate_stub_quantified_formula quants cond =
let quants' = List.map (fun (q,v,s) ->
let q' = if q = FORALL then EXISTS else FORALL in
(q',v,s)
) quants
in
let conds' = mk_not cond cond.erange in
quants', conds'
(** Visit expressions present in a formula *)
let rec visit_expr_in_formula visitor f =
bind_range f @@ fun f ->
match f with
| F_expr e -> F_expr (visit_expr visitor e)
| F_binop (op, f1, f2) -> F_binop (op, visit_expr_in_formula visitor f1, visit_expr_in_formula visitor f2)
| F_not ff -> F_not (visit_expr_in_formula visitor ff)
| F_forall (v, s, ff) -> F_forall (v, visit_set visitor s, visit_expr_in_formula visitor ff)
| F_exists (v, s, ff) -> F_exists (v, visit_set visitor s, visit_expr_in_formula visitor ff)
| F_in (e, s) -> F_in (visit_expr visitor e, visit_set visitor s)
| F_otherwise (f, e) -> F_otherwise(visit_expr_in_formula visitor f, visit_expr visitor e)
| F_if (c,f1,f2) -> F_if(visit_expr_in_formula visitor c, visit_expr_in_formula visitor f1, visit_expr_in_formula visitor f2)
and visit_set visitor s =
match s with
| S_interval (e1, e2) -> S_interval (visit_expr visitor e1, visit_expr visitor e2)
| S_resource r -> S_resource r
and visit_expr visitor e =
Visitor.map_expr visitor (fun stmt -> Keep stmt) e
let mk_stub_alloc_resource ?(mode=STRONG) res range =
mk_expr (E_stub_alloc (res,mode)) range
let negate_log_binop : log_binop -> log_binop = function
| AND -> OR
| OR -> AND
| IMPLIES -> assert false
(** {2 Pretty printers} *)
(** =-=-=-=-=-=-=-=-=-= *)
let pp_builtin = Mopsa_c_stubs_parser.Ast.pp_builtin
let pp_log_binop = Mopsa_c_stubs_parser.Ast.pp_log_binop
let pp_quantifier fmt = function
| FORALL -> pp_print_string fmt "∀"
| EXISTS -> pp_print_string fmt "∃"
let rec pp_formula fmt f =
match f.content with
| F_expr e -> pp_expr fmt e
| F_binop (op, f1, f2) -> fprintf fmt "(%a %a %a)" pp_formula f1 pp_log_binop op pp_formula f2
| F_not f -> fprintf fmt "not (%a)" pp_formula f
| F_forall (x, set, f) -> fprintf fmt "@[<v 2>∀ %a %a ∈ %a:@,%a@]" pp_typ x.vtyp pp_var x pp_set set pp_formula f
| F_exists (x, set, f) -> fprintf fmt "@[<v 2>∃ %a %a ∈ %a:@,%a@]" pp_typ x.vtyp pp_var x pp_set set pp_formula f
| F_in (x, set) -> fprintf fmt "%a ∈ %a" pp_expr x pp_set set
| F_otherwise (f, e) -> fprintf fmt "(%a otherwise %a)" pp_formula f pp_expr e
| F_if (c,f1,f2) -> fprintf fmt "if %a then %a else %a end" pp_formula c pp_formula f1 pp_formula f2
and pp_set fmt =
function
| S_interval(e1, e2) -> fprintf fmt "[%a .. %a]" pp_expr e1 pp_expr e2
| S_resource(r) -> pp_resource fmt r
and pp_interval fmt ((l,u):interval) =
fprintf fmt "[%a, %a]" pp_expr l pp_expr u
and pp_resource = Mopsa_c_stubs_parser.Ast.pp_resource
let pp_list pp sep fmt l =
pp_print_list ~pp_sep:(fun fmt () -> fprintf fmt sep) pp fmt l
let pp_opt pp fmt o =
match o with
| None -> ()
| Some x -> pp fmt x
let rec pp_local fmt local =
let local = get_content local in
fprintf fmt "local : %a %a = @[%a@];"
pp_typ local.lvar.vtyp
pp_var local.lvar
pp_local_value local.lval
and pp_local_value fmt v =
match v with
| L_new resource -> fprintf fmt "new %a" pp_resource resource
| L_call (f, args) -> fprintf fmt "%a(%a)" pp_expr f (pp_list pp_expr ", ") args
let pp_requires fmt requires =
fprintf fmt "requires : @[%a@];" pp_formula requires.content
let pp_assigns fmt assigns =
fprintf fmt "assigns : %a%a;"
pp_expr assigns.content.assign_target
(pp_print_list ~pp_sep:(fun fmt () -> ()) pp_interval) assigns.content.assign_offset
let pp_assumes fmt (assumes:assumes with_range) =
fprintf fmt "assumes : %a;" pp_formula assumes.content
let pp_ensures fmt ensures =
fprintf fmt "ensures : %a;" pp_formula ensures.content
let pp_free fmt free =
fprintf fmt "free : %a;" pp_expr free.content
let pp_message fmt msg =
match msg.content.message_kind with
| WARN -> fprintf fmt "warn: \"%s\";" msg.content.message_body
| UNSOUND -> fprintf fmt "unsound: \"%s\";" msg.content.message_body
let pp_leaf_section fmt sec =
match sec with
| S_local local -> pp_local fmt local
| S_assumes assumes -> pp_assumes fmt assumes
| S_requires requires -> pp_requires fmt requires
| S_assigns assigns -> pp_assigns fmt assigns
| S_ensures ensures -> pp_ensures fmt ensures
| S_free free -> pp_free fmt free
| S_message msg -> pp_message fmt msg
let pp_leaf_sections fmt secs =
fprintf fmt "@[<v>";
pp_print_list
~pp_sep:(fun fmt () -> fprintf fmt "@,")
pp_leaf_section
fmt secs
;
fprintf fmt "@]"
let pp_case fmt case =
fprintf fmt "@[<v 2>case \"%s\" {@,%a@]@,}"
case.case_label
pp_leaf_sections case.case_body
let pp_section fmt sec =
match sec with
| S_leaf leaf -> pp_leaf_section fmt leaf
| S_case case -> pp_case fmt case
let pp_sections fmt secs =
fprintf fmt "@[<v>";
pp_print_list
~pp_sep:(fun fmt () -> fprintf fmt "@,")
pp_section
fmt secs
;
fprintf fmt "@]"
let pp_stub_func fmt stub = pp_sections fmt stub.stub_func_body
let pp_stub_directive fmt stub = pp_sections fmt stub.stub_directive_body
(** {2 Registration of expressions} *)
let () =
register_expr_with_visitor {
compare = (fun next e1 e2 ->
match ekind e1, ekind e2 with
| E_stub_call(f1,args1), E_stub_call(f2,args2) ->
Compare.compose [
(fun () -> compare f1.stub_func_name f2.stub_func_name);
(fun () -> Compare.list compare_expr args1 args2);
]
| E_stub_builtin_call(f1, args1), E_stub_builtin_call(f2, args2) ->
Compare.compose [
(fun () -> compare f1 f2);
(fun () -> Compare.list compare_expr args1 args2)
]
| E_stub_attribute(o1, f1), E_stub_attribute(o2, f2) ->
Compare.compose [
(fun () -> compare_expr o1 o2);
(fun () -> compare f1 f2)
]
| E_stub_alloc (r1,m1), E_stub_alloc (r2,m2) ->
Compare.pair compare compare_mode (r1,m1) (r2,m2)
| E_stub_resource_mem(x1, res1), E_stub_resource_mem(x2, res2) ->
Compare.compose [
(fun () -> compare_expr x1 x2);
(fun () -> compare res1 res2);
]
| E_stub_primed(e1), E_stub_primed(e2) ->
compare_expr e1 e2
| E_stub_quantified_formula(quants1,cond1), E_stub_quantified_formula(quants2,cond2) ->
Compare.pair
(Compare.list (Compare.triple compare compare_var compare_set))
compare_expr
(quants1,cond1) (quants2,cond2)
| E_stub_otherwise (cond1, alarm1), E_stub_otherwise (cond2, alarm2) ->
Compare.pair compare_expr (Compare.option compare_expr)
(cond1, alarm1)
(cond2, alarm2)
| E_stub_if(c1,fthen1,felse1), E_stub_if(c2,fthen2,felse2) ->
Compare.triple compare_expr compare_expr compare_expr
(c1, fthen1, felse1)
(c2, fthen2, felse2)
| E_stub_raise msg1, E_stub_raise msg2 ->
String.compare msg1 msg2
| _ -> next e1 e2
);
visit = (fun next e ->
match ekind e with
| E_stub_call (f,args) ->
{ exprs = args; stmts = [] },
(function {exprs = args} -> {e with ekind = E_stub_call(f, args)})
| E_stub_return -> leaf e
| E_stub_builtin_call(f, args) ->
{ exprs = args; stmts = [] },
(function {exprs} -> {e with ekind = E_stub_builtin_call(f, exprs)})
| E_stub_attribute(o, f) ->
{ exprs = [o]; stmts = [] },
(function { exprs = [o] } -> { e with ekind = E_stub_attribute(o, f) } | _ -> assert false)
| E_stub_alloc _ -> leaf e
| E_stub_resource_mem(x, res) ->
{ exprs = [x]; stmts = []},
(function { exprs = [x] } -> { e with ekind = E_stub_resource_mem(x, res) } | _ -> assert false)
| E_stub_primed(ee) ->
{ exprs = [ee]; stmts = [] },
(function { exprs = [ee] } -> { e with ekind = E_stub_primed(ee) } | _ -> assert false)
| E_stub_quantified_formula(quants,cond) ->
let rec decompose_quants quants =
match quants with
| [] -> []
| (_,_,S_interval(hi,lo))::tl -> hi::lo::decompose_quants tl
| (_,_,S_resource _)::tl -> decompose_quants tl
in
let rec recompose_quants quants bounds =
match quants, bounds with
| [], [] -> []
| (q,v,S_interval _)::tl1, lo::hi::tl2 -> (q,v,S_interval(lo,hi))::recompose_quants tl1 tl2
| (q,v,S_resource r)::tl1, l2 -> (q,v,S_resource r)::recompose_quants tl1 l2
| _ -> assert false
in
{ exprs = decompose_quants quants @ [cond]; stmts = [] },
(function { exprs } ->
let rexprs = List.rev exprs in
let cond = List.hd rexprs and quants = recompose_quants quants (List.rev @@ List.tl rexprs) in
{ e with ekind = E_stub_quantified_formula(quants,cond) })
| E_stub_otherwise (cond, None) ->
{ exprs = [cond]; stmts = [] },
(function {exprs} ->
let cond = match exprs with [e] -> e | _ -> assert false in
{ e with ekind = E_stub_otherwise (cond, None) })
| E_stub_otherwise (cond, Some alarm) ->
{ exprs = [cond;alarm]; stmts = [] },
(function {exprs} ->
let cond,alarm = match exprs with [e1;e2] -> e1,e2 | _ -> assert false in
{ e with ekind = E_stub_otherwise (cond, Some alarm) })
| E_stub_if (c, f1, f2) ->
{ exprs = [c;f1;f2]; stmts = [] },
(function {exprs} ->
let c,f1,f2 = match exprs with [e0;e1;e2] -> e0,e1,e2 | _ -> assert false in
{ e with ekind = E_stub_if (c,f1,f2) })
| E_stub_raise msg -> leaf e
| _ -> next e
);
print = (fun next fmt e ->
match ekind e with
| E_stub_call (s, args) -> fprintf fmt "stub %s(%a)" s.stub_func_name (pp_list pp_expr ", ") args
| E_stub_return -> pp_print_string fmt "return"
| E_stub_builtin_call(f, args) -> fprintf fmt "%a(%a)" pp_builtin f (pp_list pp_expr ", ") args
| E_stub_attribute(o, f) -> fprintf fmt "%a:%s" pp_expr o f
| E_stub_alloc (r,STRONG) -> fprintf fmt "alloc res(%s)" r
| E_stub_alloc (r,WEAK) -> fprintf fmt "alloc res(%s):weak" r
| E_stub_resource_mem(x, res) -> fprintf fmt "%a ∈ %a" pp_expr x pp_resource res
| E_stub_primed(ee) -> fprintf fmt "%a'" pp_expr ee
| E_stub_quantified_formula(quants,cond) ->
fprintf fmt "%a : %a"
(pp_print_list ~pp_sep:(fun fmt () -> pp_print_string fmt ", ")
(fun fmt (q,v,s) -> fprintf fmt "%a%a ∈ %a" pp_quantifier q pp_var v pp_set s)
) quants
pp_expr cond
| E_stub_otherwise(cond,None) -> pp_expr fmt cond
| E_stub_otherwise(cond,Some alarm) -> fprintf fmt "(%a otherwise %a)" pp_expr cond pp_expr alarm
| E_stub_if(c,f1,f2) -> fprintf fmt "(if %a then %a else %a end)" pp_expr c pp_expr f1 pp_expr f2
| E_stub_raise msg -> fprintf fmt "raise(\"%s\")" msg
| _ -> next fmt e
);
}
(** {2 Registration of statements} *)
let () =
register_stmt_with_visitor {
compare = (fun next s1 s2 ->
match skind s1, skind s2 with
| S_stub_directive (stub1), S_stub_directive (stub2) ->
panic "compare for stubs not supported"
| S_stub_free(e1), S_stub_free(e2) ->
compare_expr e1 e2
| S_stub_assigns a1, S_stub_assigns a2 -> compare_assigns a1 a2
| S_stub_prepare_all_assigns a1, S_stub_prepare_all_assigns a2
| S_stub_clean_all_assigns a1, S_stub_clean_all_assigns a2 ->
Compare.list compare_assigns a1 a2
| S_stub_requires(e1), S_stub_requires(e2) ->
compare_expr e1 e2
| _ -> next s1 s2
);
visit = (fun next s ->
match skind s with
| S_stub_directive _ -> leaf s
| S_stub_free e ->
{ exprs = [e]; stmts = [] },
(function { exprs = [e] } -> { s with skind = S_stub_free e } | _ -> assert false)
| S_stub_assigns a ->
let lbounds = List.map fst a.assign_offset in
let hbounds = List.map snd a.assign_offset in
{ exprs = a.assign_target::lbounds@hbounds; stmts = [] },
(function
| { exprs = assign_target::bounds } ->
let lbounds,hbounds = ListExt.split bounds in
let assign_offset = List.combine lbounds hbounds in
{ s with skind = S_stub_assigns {assign_target; assign_offset} }
| _ -> assert false)
| S_stub_prepare_all_assigns _ -> leaf s
| S_stub_clean_all_assigns _ -> leaf s
| S_stub_requires e ->
{ exprs = [e]; stmts = [] },
(function { exprs = [e] } -> { s with skind = S_stub_requires e } | _ -> assert false)
| _ -> next s
);
print = (fun next fmt s ->
match skind s with
| S_stub_directive (stub) ->
fprintf fmt "@[<v 2>/*$!@,%a@]*/"
pp_sections stub.stub_directive_body
| S_stub_free e -> fprintf fmt "stub-free(%a);" pp_expr e
| S_stub_assigns assigns ->
fprintf fmt "assigns : %a%a;"
pp_expr assigns.assign_target
(pp_print_list ~pp_sep:(fun fmt () -> ())
(fun fmt (l, u) ->
fprintf fmt "[%a .. %a]" pp_expr l pp_expr u
)
) assigns.assign_offset
| S_stub_prepare_all_assigns _ -> fprintf fmt "prepare assigns;"
| S_stub_clean_all_assigns _ -> fprintf fmt "clean assigns;"
| S_stub_requires e ->
fprintf fmt "requires %a;" pp_expr e
| _ -> next fmt s
);
}