Source file StmtSemantics.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
779
780
781
782
783
784
785
786
787
788
789
790
791
open Sigs
open Cil_types
open Cil_datatype
open Clabels
let not_yet = Wp_parameters.not_yet_implemented
module Make(Compiler:Sigs.Compiler) =
struct
module Compiler = Compiler
module Cfg = CfgCompiler.Cfg(Compiler.M.Sigma)
module M = Compiler.M
module Sigma = Compiler.M.Sigma
module C = Compiler.C
module L = Compiler.L
module A = Compiler.A
type node = Cfg.node
type goal = {
goal_pred : Cfg.P.t;
goal_prop : WpPropId.prop_id;
}
type cfg = Cfg.cfg
type paths = {
paths_cfg : cfg;
paths_goals : goal Bag.t;
}
type env = {
flow : node LabelMap.t ;
kf : Kernel_function.t;
result : Lang.F.var;
return : typ ;
(** used for substituting directly values without going through terms.
Good for memory models, avoid unneeded conversions. *)
subst_formals: (exp * node) Varinfo.Map.t;
status : Lang.F.var;
}
exception LabelNotFound of c_label
let result env = env.result
let bind l n env =
{ env with flow = LabelMap.add l n env.flow }
let (@^) cfg1 cfg2 = {
paths_cfg = Cfg.concat cfg1.paths_cfg cfg2.paths_cfg;
paths_goals = Bag.concat cfg1.paths_goals cfg2.paths_goals;
}
let (@*) env lns =
let flow =
List.fold_left (fun flow (l, n) -> LabelMap.add l n flow) env.flow lns
in { env with flow }
let (@:) env lbl =
try
LabelMap.find lbl env.flow
with Not_found -> raise (LabelNotFound lbl)
let (@-) env f =
{ env with flow = LabelMap.filter (fun lbl _ -> f lbl) env.flow }
let empty_env kf =
let return = Kernel_function.get_return_type kf in
let result = Lang.freshvar ~basename:"result" (Lang.tau_of_ctype return) in
let status = Lang.freshvar ~basename:"status" Qed.Logic.Int in
let env = {flow = LabelMap.empty; kf; result; status; return;
subst_formals = Varinfo.Map.empty} in
env @* [
Clabels.init, Cfg.node ();
Clabels.exit, Cfg.node();
]
let paths_of_cfg cfg = {
paths_cfg = cfg;
paths_goals = Bag.empty;
}
let nop = Cfg.nop |> paths_of_cfg
let add_tmpnode n = Cfg.add_tmpnode n |> paths_of_cfg
let goto n1 n2 = (Cfg.goto n1 n2) |> paths_of_cfg
let meta ?stmt ?descr n = (Cfg.meta ?stmt ?descr n) |> paths_of_cfg
let guard nc c nt = (Cfg.guard nc c nt) |> paths_of_cfg
let guard' nc c nt = (Cfg.guard' nc c nt) |> paths_of_cfg
let either n ns = (Cfg.either n ns) |> paths_of_cfg
let implies n ns = (Cfg.implies n ns) |> paths_of_cfg
let memory_effect n1 e n2 = (Cfg.memory_effect n1 e n2) |> paths_of_cfg
let assume p = (Cfg.assume p) |> paths_of_cfg
let current env sigma =
Cfg.Node.(Map.add (env @: Clabels.here) sigma Map.empty)
let goals_nodes goals =
Bag.fold_left (fun acc g ->
Cfg.Node.Map.fold
(fun n _ acc -> Cfg.Node.Set.add n acc)
(Cfg.P.reads g.goal_pred) acc
)
Cfg.Node.Set.empty
goals
let rec sequence f env = function
| [] -> goto (env @: Clabels.here) (env @: Clabels.next)
| [ elt ] -> f env elt
| stmt :: stmts ->
let n = Cfg.node () in
let paths = f (bind Clabels.next n env) stmt in
paths @^ (sequence f (bind Clabels.here n env) stmts)
let choice ?(pre=Clabels.here) ?(post=Clabels.next) f env =
let pre_node = env @: pre in
let apply f env elt =
let n = Cfg.node () in
n, f (bind pre n env) elt in
let rec aux env ns = function
| [] -> goto (env @: pre) (env @: post)
| [ elt ] ->
let n, paths = apply f env elt in
paths @^ either pre_node (n :: ns)
| elt :: elts ->
let n, paths = apply f env elt in
paths @^ (aux env (n :: ns) elts)
in
aux env []
(** executed possibly at the same time *)
let parallel ?(pre=Clabels.here) ?(post=Clabels.next) f env =
let pre_node = env @: pre in
let apply f env elt =
let n = Cfg.node () in
n, f (bind pre n env) elt in
let rec aux env ns = function
| [] -> goto (env @: pre) (env @: post)
| [ elt ] ->
let n, (c,paths) = apply f env elt in
paths @^ implies pre_node ((c,n) :: ns)
| elt :: elts ->
let n, (c,paths) = apply f env elt in
paths @^ (aux env ((c,n) :: ns) elts)
in
aux env []
let scope env sc xs =
let post = Sigma.create () in
let pre = M.alloc post xs in
let seq = { pre ; post } in
let p = Lang.F.p_conj (M.scope seq sc xs) in
let e = Cfg.E.create seq p in
let descr =
Format.asprintf "%s scope [%a]: @[%a@]"
(match sc with Leave -> "Leaving" | Enter -> "Entering")
(Pretty_utils.pp_iter ~sep:"; @" List.iter Varinfo.pretty) xs
Cfg.E.pretty e
in
meta ~descr (env @: Clabels.here)
@^ memory_effect (env @: Clabels.here) e (env @: Clabels.next)
let set env lv exp =
let here = Sigma.create () in
let loc = C.lval here lv in
let value = C.exp here exp in
let obj = Ctypes.object_of (Cil.typeOfLval lv) in
let next = Sigma.havoc here (M.domain obj loc) in
let sequence = { pre=here ; post=next } in
let ps =
match value with
| Loc ptr -> M.copied sequence obj loc ptr
| Val term -> M.stored sequence obj loc term in
let ps = List.map Cvalues.equation ps in
let e = Cfg.E.create sequence (Lang.F.p_conj ps) in
let descr = Format.asprintf "Set: @[%a = %a@]"
Printer.pp_lval lv Printer.pp_exp exp in
meta ~descr (env @: Clabels.here)
@^ memory_effect ( env @: Clabels.here ) e (env @: Clabels.next)
let return env e_opt =
goto (env @: Clabels.here) (env @: Clabels.next)
@^
match e_opt with
| None -> nop
| Some exp ->
let rtyp = env.return in
let here = Sigma.create () in
let value = C.return here rtyp exp in
let p = Lang.F.p_equal (Lang.F.e_var env.result) value in
assume (Cfg.P.create (current env here) p)
let mk_frame ~descr env =
let nsigmas =
LabelMap.fold
(fun _ (n : node) (nmap : M.sigma Cfg.Node.Map.t) ->
if Cfg.Node.Map.mem n nmap then nmap
else Cfg.Node.Map.add n (Sigma.create ()) nmap)
env.flow
Cfg.Node.Map.empty
in
let lsigmas =
LabelMap.map
(fun n ->
try Cfg.Node.Map.find n nsigmas
with Not_found -> assert false )
env.flow
in
let frame_formals = L.mk_frame
~kf:env.kf
~descr:"frame_formals"
~labels:LabelMap.empty
()
in
let formals = Varinfo.Map.map (fun (exp,n) ->
try
let here = Cfg.Node.Map.find n nsigmas in
L.in_frame frame_formals (C.exp here) exp
with Not_found -> Wp_parameters.fatal "node of formals not present in labels. normal?"
) env.subst_formals
in
let frame =
L.mk_frame
~labels:lsigmas ~kf:env.kf
~result:(Sigs.R_var env.result)
~status:env.status
~formals ~descr ()
in
frame, nsigmas, lsigmas
let pred
: env -> Sigs.polarity -> predicate -> _
= fun env polarity p ->
let frame, nsigmas, lsigmas = mk_frame ~descr:"pred" env in
try
let here = LabelMap.find Clabels.here lsigmas in
let lenv = L.mk_env ~here () in
let pred = L.in_frame frame (L.pred polarity lenv) p in
let nsigmas = Cfg.Node.Map.filter (fun _ s ->
s == here || not (Sigma.Chunk.Set.is_empty (Sigma.domain s))
) nsigmas
in
(Cfg.P.create nsigmas pred)
with Not_found -> Wp_parameters.fatal "Error during compilation"
let assert_ env p prop_id =
let pos = pred env `Positive p.ip_content.tp_statement in
let env' = env @* [Clabels.here, env @: Clabels.next ] in
let neg = pred env' `Negative p.ip_content.tp_statement in
let goal = {
goal_pred = pos;
goal_prop = prop_id;
} in
{
paths_goals = Bag.elt goal;
paths_cfg = Cfg.goto (env @: Clabels.here) (env @: Clabels.next);
} @^ assume neg
let assume_
: env -> Sigs.polarity -> predicate -> paths
= fun env polarity p ->
assume (pred env polarity p)
let rec call_kf
: env -> lval option -> kernel_function -> exp list -> paths
= fun env lvr kf es ->
let pre_node = Cfg.node () in
let post_node = Cfg.node () in
let return_node = Cfg.node () in
let next_node = env @: Clabels.next in
let exit_stop = Cfg.node () in
let cfg_enter_scope =
scope
(env @* [Clabels.next,pre_node])
Enter (Kernel_function.get_formals kf)
in
let cfg_leave_scope =
scope
(env @* [Clabels.here,post_node;Clabels.next,return_node])
Leave (Kernel_function.get_formals kf)
in
let cfg_contract env =
spec env (Annotations.funspec kf)
in
let result env = match lvr with
| None -> goto (env @: Clabels.here) (env @: Clabels.next)
| Some lv ->
let pre = Sigma.create () in
let tr = Cil.typeOfLval lv in
let obj = Ctypes.object_of tr in
let loc = C.lval pre lv in
let post = Sigma.havoc pre (M.domain obj loc) in
let vr = M.load post obj loc in
let p =
C.equal_typ tr vr
(C.cast tr env.return (Val (Lang.F.e_var env.result)))
in
let e = Cfg.E.create { pre; post } p in
memory_effect (env @: Clabels.here) e (env @: Clabels.next)
in
let old_status = env.status in
let exit_status (env:env) =
let p = Lang.F.p_equal (Lang.F.e_var old_status) (Lang.F.e_var env.status) in
let s = M.Sigma.create () in
let e = Cfg.E.create {pre=s;post=s} p in
memory_effect (env @: Clabels.here) e (env @: Clabels.next)
in
let subst_formals = List.fold_left2
(fun acc v e -> Varinfo.Map.add v (e,pre_node) acc)
Varinfo.Map.empty (Kernel_function.get_formals kf) es
in
let env_call =
{ (empty_env kf) with subst_formals }
@* [Clabels.init, env @: Clabels.init;
Clabels.pre, pre_node; Clabels.here, pre_node;
Clabels.next, post_node; Clabels.post, post_node;
Clabels.exit, env @: Clabels.exit]
in
nop
@^ cfg_enter_scope
@^ cfg_contract env_call
@^ cfg_leave_scope
@^ result (env_call @* [(Clabels.here, return_node);
(Clabels.next, next_node)])
@^ exit_status (env_call @* [(Clabels.here, exit_stop);
(Clabels.next, env @: Clabels.exit)])
and call
: env -> lval option -> exp -> exp list -> paths
= fun env lv e es ->
match Kernel_function.get_called e with
| Some kf -> call_kf env lv kf es
| None -> not_yet "[StmtSemantics] Call through a function pointer."
and instr : env -> instr -> paths = fun env -> function
| Set (lv, e, _) -> set env lv e
| Call (lv, e, es, _) -> call env lv e es
| Asm _ -> not_yet "[StmtSemantics] Inline Asm."
| Local_init (v, ConsInit(f, args, kind), loc) ->
Cil.treat_constructor_as_func
(fun lv e es _ -> call env lv e es)
v f args kind loc
| Local_init (vi, AssignInit init, _) ->
let here = Sigma.create () in
let next = Sigma.create () in
let init = C.init ~sigma:next vi (Some init) in
let hyp_value = Lang.F.p_all (fun (_, h) -> fst h) init in
let hyp_init = Lang.F.p_all (fun (_, h) -> snd h) init in
let hyp = Lang.F.p_and hyp_init hyp_value in
memory_effect (env @: Clabels.here) (Cfg.E.create {pre=here; post=next} hyp) (env @: Clabels.next)
| Skip _ | Code_annot _ -> goto (env @: Clabels.here) (env @: Clabels.next)
and spec : env -> spec -> paths = fun env spec ->
let pre_cond env p prop_id =
assert_ env p prop_id
in
let post_cond termination_kind env (tk, ip) =
if tk = termination_kind then
assume_ env `Positive ip.ip_content.tp_statement
else nop
in
let behavior env b =
let nrequires = Cfg.node () in
let nassigns = Cfg.node () in
let assume =
let p = pred (env @* [Clabels.here, env @: Clabels.pre])
`Negative (Ast_info.behavior_assumes b) in
match Cfg.P.to_condition p with
| Some (c,None) -> c
| Some (c,Some n) when Cfg.Node.equal n (env @: Clabels.pre) -> c
| _ -> not_yet "assume of behaviors with labels: %a" Cfg.P.pretty p
in
let post_normal_behavior = Cfg.node () in
let post_normal_env = env @* [Clabels.here, nassigns;
Clabels.post, post_normal_behavior] in
let post_at_exit_behavior = Cfg.node () in
let post_at_exit_env = env @* [Clabels.here, nassigns;
Clabels.exit, post_at_exit_behavior] in
assume,
sequence
(fun env ip ->
let prop_id = WpPropId.mk_pre_id env.kf Kglobal b ip in
pre_cond env ip prop_id)
(env @* [Clabels.next, nrequires]) b.b_requires
@^ assigns (env @* [Clabels.here, nrequires; Clabels.next, nassigns]) b.b_assigns
@^ either nassigns [post_normal_behavior;post_at_exit_behavior]
@^ List.fold_left
(fun acc post -> acc @^ post_cond Normal post_normal_env post)
nop b.b_post_cond
@^ List.fold_left
(fun acc post -> acc @^ post_cond Exits post_at_exit_env post)
nop b.b_post_cond
@^ goto post_normal_behavior (env @: Clabels.post)
@^ goto post_at_exit_behavior (env @: Clabels.exit)
in
let env = env @* [Clabels.here, env @: Clabels.pre; Clabels.next, env @: Clabels.post] in
parallel behavior env spec.spec_behavior
and assigns : env -> assigns -> paths = fun env a ->
let frame, _, _ = mk_frame ~descr:"assigns" env in
let lenv = L.mk_env () in
let here = Sigma.create () in
let authorized_region = L.in_frame frame
(L.assigned_of_assigns lenv) a in
match authorized_region with
| None -> goto (env @: Clabels.here) (env @: Clabels.next)
| Some region ->
let domain = A.domain region in
let next = M.Sigma.havoc here domain in
let seq = { pre = here; post = next } in
let preds = A.apply_assigns seq region in
memory_effect (env @: Clabels.here) (Cfg.E.create seq (Lang.F.p_conj preds)) (env @: Clabels.next)
and froms : env -> from list -> paths = fun env froms ->
assigns env (Writes froms)
let pref v1 v2 =
let open Interpreted_automata in
match v1.vertex_info, v2.vertex_info with
| NoneInfo, NoneInfo -> 0
| NoneInfo, _ -> -1
| _ , NoneInfo -> 1
| LoopHead i, LoopHead j -> Stdlib.compare j i
module Automata = Interpreted_automata.UnrollUnnatural.Version
type nodes = {
global: node Automata.Hashtbl.t;
local: node Automata.Map.t;
}
let get_node nodes v =
try Automata.Map.find v nodes.local
with Not_found ->
Automata.Hashtbl.memo nodes.global v (fun _ -> Cfg.node ())
let add_local nodes v n =
{nodes with local = Automata.Map.add v n nodes.local}
let transition
: env -> nodes -> Automata.t Interpreted_automata.transition -> paths
= fun env nodes tr ->
let open Interpreted_automata in
match tr with
| Skip | Enter { blocals = [] } | Leave { blocals = [] } ->
goto (env @: Clabels.here) (env @: Clabels.next)
| Enter {blocals} -> scope env Sigs.Enter blocals
| Leave {blocals} -> scope env Sigs.Leave blocals
| Return (r,_) -> return env r
| Prop ({kind = Assert|Invariant} as a, _) ->
let env = Logic_label.Map.fold
(fun logic_label vertex acc ->
let c_label = Clabels.of_logic logic_label in
let node = get_node nodes vertex in
bind c_label node acc
) a.labels env in
assert_ env a.predicate (WpPropId.mk_property a.property)
| Prop ({kind = Assume} as a, _)->
let env = Logic_label.Map.fold
(fun logic_label vertex acc ->
let c_label = Clabels.of_logic logic_label in
let node = get_node nodes vertex in
bind c_label node acc
) a.labels env in
assume (pred env `Negative a.predicate.ip_content.tp_statement) @^
goto (env @: Clabels.here) (env @: Clabels.next)
| Prop _ ->
not_yet "[StmtSemantics] Annots other than 'assert'"
| Guard (exp,b,_) ->
let here = Sigma.create () in
let cond = C.cond here exp in
let condition = Cfg.C.create here cond in
(if b = Then then guard else guard')
(env @: Clabels.here) condition (env @: Clabels.next)
| Instr (i,_) -> instr env i
let rec get_invariants g n (l:Automata.t Wto.partition) =
let open Interpreted_automata in
let open Interpreted_automata.UnrollUnnatural in
match l, G.succ_e g n with
| (Wto.Node a)::l,
[(_,{edge_transition =
(Prop({kind=Assert|Invariant|Assume|Check},_) | Skip) as t},b)]
when Automata.equal a b ->
let invs,l = get_invariants g b l in
(t,a)::invs,l
| _ -> [],(Wto.Node n)::l
let as_assumes l =
let open Interpreted_automata in
List.map (function
| (Prop({kind=Assume},_),_) as t -> t
| (Prop({kind=Assert|Invariant} as a,s),b) -> (Prop ({a with kind=Assume},s),b)
| (Prop({kind=Check},_),b) -> (Skip,b)
| (Skip,_) as t -> t
| _ -> assert false
) l
let automaton : env -> Interpreted_automata.automaton -> paths = fun env a ->
let open Interpreted_automata in
let binder = M.configure_ia a in
let bind = binder.bind in
let wto = WTO.partition ~pref ~init:a.entry_point ~succs:(G.succ a.graph) in
let index = Compute.build_wto_index_table wto in
let open UnrollUnnatural in
let g = unroll_unnatural_loop a wto index in
let here = (a.entry_point,Vertex.Set.empty) in
let next = (a.return_point,Vertex.Set.empty) in
let wto =
WTO.partition
~pref:(fun _ _ -> 0)
~succs:(UnrollUnnatural.G.succ g)
~init:here in
let do_node nodes v paths =
let n = get_node nodes v in
let l,paths = G.fold_succ_e (fun (_,e,v2) (l,paths) ->
let n2' = Cfg.node () in
let n2 = get_node nodes v2 in
(n2'::l, transition (env @* [Clabels.here,n2';Clabels.next,n2]) nodes e.edge_transition
@^ add_tmpnode n2'
@^ paths)
) g v ([],paths) in
(either n l) @^ paths
in
let rec do_list ~fresh_nodes paths nodes n1 = function
| [] -> (n1,paths)
| (t,b)::l ->
let n2, nodes =
if fresh_nodes then
let n2 = Cfg.node () in
let nodes = add_local nodes b n2 in
n2, nodes
else (get_node nodes b), nodes
in
let paths = paths @^ transition (env @* [Clabels.here,n1;Clabels.next,n2]) nodes t in
do_list ~fresh_nodes paths nodes n2 l
in
let rec component nodes paths = function
| Wto.Node ((n, _) as v) -> bind n (do_node nodes v) paths
| Wto.Component ((n, _) as v, l) ->
let do_component (v, l) =
assert (not (Automata.Map.mem v nodes.local));
let invariants,l = get_invariants g v l in
let n = get_node {nodes with local = Automata.Map.empty} v in
let n,paths = do_list ~fresh_nodes:true paths nodes n invariants in
let n_loop = Cfg.node () in
let _,paths = do_list ~fresh_nodes:true paths nodes n_loop invariants in
let n_havoc = Cfg.node () in
let havoc = Cfg.havoc n ~memory_effects:{pre=n_havoc;post=n_loop} n_havoc in
let paths = (havoc |> paths_of_cfg) @^ paths in
let invariants_as_assumes = as_assumes invariants in
let _,paths =
do_list ~fresh_nodes:false paths (add_local nodes v n_havoc)
n_havoc invariants_as_assumes in
partition (add_local nodes v n_loop) paths l
in
bind n do_component (v, l)
and partition nodes paths l =
List.fold_left (component nodes) paths l
in
let nodes = {
global = Automata.Hashtbl.create 10;
local = Automata.Map.empty
} in
Automata.Hashtbl.add nodes.global here (env @: Clabels.here);
Automata.Hashtbl.add nodes.global next (env @: Clabels.next);
partition nodes nop wto
(** connect init to here. [is_pre_main] indicate if here is the
pre-state of main. *)
let init ~is_pre_main env =
let ninit = (env @: Clabels.init) in
let sinit = Sigma.create () in
let cfg_init = Globals.Vars.fold_in_file_order
(fun var initinfo cfg ->
if var.vstorage = Extern then cfg else
let init = C.init ~sigma:sinit var initinfo.init in
let hvalue = Lang.F.p_all (fun (_, h) -> fst h) init in
let hinit = Lang.F.p_all (fun (_, h) -> snd h) init in
let h = Lang.F.p_and hvalue hinit in
let h = Cfg.P.create
(Cfg.Node.Map.add ninit sinit Cfg.Node.Map.empty)
h
in
assume h
) nop
in
if is_pre_main
then cfg_init @^ goto ninit (env @: Clabels.here)
else
let nconst = Cfg.Node.create () in
let sconst = Sigma.havoc_any ~call:false sinit in
let havoc = Cfg.E.create {pre=sinit; post=sconst} Lang.F.p_true in
let consts =
if Wp_parameters.Init.get () then
Globals.Vars.fold_in_file_order
(fun var _ cfg ->
if Cil.isGlobalInitConst var
then
let h = (C.unchanged sconst sinit var) in
let h = Cfg.P.create
(Cfg.Node.Map.add ninit sinit
(Cfg.Node.Map.add nconst sconst
Cfg.Node.Map.empty))
h
in
cfg @^ assume h
else cfg
) nop
else nop
in
cfg_init @^ memory_effect ninit havoc nconst @^ consts @^ goto nconst (env @: Clabels.here)
let pre_spec env spec =
let pre_cond polarity env p =
assume_ (env @* [Clabels.here, env @: Clabels.pre]) polarity p
in
let behavior env b =
let assume =
let p = pred env `Negative (Ast_info.behavior_assumes b) in
match Cfg.P.to_condition p with
| Some (c,None) -> c
| Some (c,Some n) when Cfg.Node.equal n (env @: Clabels.here) -> c
| _ -> not_yet "assume of behaviors with labels: %a" Cfg.P.pretty p
in
assume,
List.fold_left
(fun acc ip -> acc @^ pre_cond `Negative env ip.ip_content.tp_statement)
nop b.b_requires
@^ goto (env @: Clabels.here) (env @: Clabels.next)
in
parallel behavior env spec.spec_behavior
let post_normal_spec env spec =
let post_cond termination_kind env (tk, ip) propid =
if tk = termination_kind then
assert_ env ip propid
else nop
in
let behavior env b =
let assume =
let p = pred (env @* [Clabels.here, env @: Clabels.pre])
`Negative (Ast_info.behavior_assumes b)
in
match Cfg.P.to_condition p with
| Some (c,None) -> c
| Some (c,Some n) when Cfg.Node.equal n (env @: Clabels.pre) -> c
| _ -> not_yet "assume of behaviors with labels: %a" Cfg.P.pretty p
in
assume,
sequence
(fun env post ->
let propid = WpPropId.mk_fct_post_id env.kf b post in
post_cond Normal env post propid)
env b.b_post_cond
in
let env = env in
parallel behavior env spec.spec_behavior
let compute_kf kf =
let open Interpreted_automata in
let autom = Compute.get_automaton ~annotations:true kf in
let binder = M.configure_ia autom in
let bind = binder.bind in
let spec = Annotations.funspec kf in
let pres = { pre = Cfg.node (); post = Cfg.node () } in
let posts = { pre = Cfg.node (); post = Cfg.node () } in
let env = empty_env kf @* [Clabels.pre,pres.post;Clabels.post,posts.pre] in
let init =
init ~is_pre_main:(CfgInfos.is_entry_point kf)
(env @* [Clabels.here,pres.pre]) in
let pre =
bind autom.entry_point @@
pre_spec (env @* [Clabels.here,pres.pre;Clabels.next,pres.post])
in
let paths =
automaton (env @* [Clabels.here,pres.post;Clabels.next,posts.pre]) autom
in
let post =
bind autom.return_point @@
post_normal_spec (env @* [Clabels.here,posts.pre;Clabels.next,posts.post])
in
init @^ pre spec @^ paths @^ post spec, env @: Clabels.init
end