-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathsymbsimp.ml
executable file
·3073 lines (2921 loc) · 128 KB
/
symbsimp.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
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
(* Poling: Proof Of Linearizability Generator
* Poling is built on top of CAVE and shares the same license with CAVE
* See LICENSE.txt for license.
* Contact: He Zhu, Department of Computer Science, Purdue University
* Email: zhu103@purdue.edu
*)
(******************************************************************************)
(* __ ___ CAVE: Concurrent Algorithm VErifier *)
(* / /\ \ / | Copyright (c) 2010, Viktor Vafeiadis *)
(* | /--\ \ / |--- *)
(* \__ / \ \/ |___ See LICENSE.txt for license. *)
(* *)
(******************************************************************************)
(** Symbolic execution *)
open Misc
open Exp
open Assertions
open Commands
open Genarith
(* -------------------------------------------------------------------------- *)
(** {2 Shorthands} *)
(* -------------------------------------------------------------------------- *)
let (@%) ((pl,sl),scpl) pl' = ((Pure.conj pl' pl,sl),scpl)
let (@&) = Pure.conj_one
let (@@***) x y = eprop_star_assume x y
let (@@**) x y = eprop_star x y
let (@@&&) x y = cprop_pure x @@** y
let (@@&) x y = Pure.one x @@&& y
let print loc = Location.print (!Misc.formatter) loc; pp
let pp_generated_function fname n =
if Genarith.enabled () then pp_function !Misc.formatter (fname,n)
let cform_to_sub ((p,_),_) = Pure.to_sub p
(* -------------------------------------------------------------------------- *)
(** {2 Arguments} *)
(* -------------------------------------------------------------------------- *)
(**
If [verbose >= 1]
If [verbose >= 2], print loop invariants & actions inferred.
If [verbose >= 3], print verification condition & action inference.
If [verbose >= 4], print intermediate states.
If [verbose >= 5], print stabilizations.
If [verbose >= 6], print inferred frames.
*)
let verbose = ref 1
let left_mover_opt = ref false
(**
If [infer >= 1], perform action inference.
If [infer >= 2], perform linearization point inference. *)
let infer = ref 1
(** If [mcpa_infr >= 1], perform mcpa linearization point inference *)
let mcpa_infer = ref 0
let args =
[("-v", Arg.Set_int verbose, "<n> Display internal information (symbolic execution)");
("-lm", Arg.Set left_mover_opt, " Enable left mover optimization");
("-no_infer_RG", Arg.Unit (fun () -> infer := 0), " Do not infer rely/guarantee specifications");
("-infer_RG", Arg.Unit (fun () -> infer := 1), " Infer rely/guarantee specifications");
("-linear_reuse", Arg.Unit (fun () -> infer := 2), " Infer linearization points");
("-linear", Arg.Unit (fun () -> infer := 3), " Infer linearization points");
("-mcpa_linear", Arg.Unit (fun () -> mcpa_infer := 1), " MCPA Infer linearization points")]
let qs_given = ref false
let ps_given = ref false
let inv_given = ref false
let pp_line () =
if !verbose >= 1 then
pp "----------------------------------------------------------------------------@."
let pp_comment s =
if !verbose >= 1 then begin
pp "@.";
if Genarith.enabled () then pp "// ";
pp "%s@." s
end
let pp_internal_error () =
pp "@.Internal error: please report.@."
(* -------------------------------------------------------------------------- *)
(** {2 Error handling} *)
(* -------------------------------------------------------------------------- *)
(** Internal exception *)
exception Symbolic_execution_error
let error_noframe loc s cp1 cp2 =
if !verbose >= 1 then
print loc "ERROR cannot find frame: %s@.@[<hv>@[<hov 2>%a@]@ |-@ @[<hov 2>%a@]@]@." s
pp_cprop cp1 pp_cprop cp2;
raise Symbolic_execution_error
let error_noframe_ext loc s ep1 cp2 =
error_noframe loc s (List.map cform_of_eform ep1) cp2
let test_leakmem ?(warn=true) loc cp =
if is_cprop_empty cp then ()
else if !allow_leaks then begin
if !verbose >= 1 && warn then
(*print loc "WARNING memory leak:@.%a@." pp_cprop cp*) ()
else ()
end else begin
if !verbose >= 1 then print loc "ERROR memory leak:@.%a@." pp_cprop cp;
raise Symbolic_execution_error
end
let error_heap loc e ep =
if !verbose >= 1 then
print loc "ERROR: %a is possibly unallocated in@.%a@."
pp_exp e pp_eprop ep;
raise Symbolic_execution_error
let error_heap2 loc s ep =
if !verbose >= 1 then
print loc "ERROR: %s with precondition@.%a@." s pp_eprop ep;
raise Symbolic_execution_error
(* -------------------------------------------------------------------------- *)
(** {2 Global variables} *)
(* -------------------------------------------------------------------------- *)
type global_env =
{ g_prover : prover
; g_abstraction : abstraction
; g_globals : IdSet.t
; g_fun_ht : (string, fun_info) Hashtbl.t
; g_res_ht : (component, act list) Hashtbl.t
; g_renv : (component, cprop) Hashtbl.t
; mutable g_guarantee :
(component * (string * Pure.t * can_spatial * can_spatial * can_spatial)) list
; mutable g_guar_changed : bool
; mutable g_params : IdSet.t
; mutable g_no_interf_hack : bool (** Assume no interference occurs *)
; g_linear_pre : cprop option (** Fail quickly for linearizability checking *)
; cand_lin_point : (string,
(** 1 eff loc 2 precondition 3 exe st 4 valid lp?*)
(Location.t * (Predicate.t * (Location.t *
(Predicate.t list * cprop * fld_assignments * IdSet.t * bool)) list)) list) Hashtbl.t
(** Remember the effectful linearization points *)
; non_eff_postconditions : (string,
(** 1 return loc, 2 pureinfo 3 noneff witnesses *)
(Location.t * (Predicate.t * (Location.t * cprop) list)) list) Hashtbl.t
; rdefs : (component, Predicate.t) Hashtbl.t (** The user defined concrete set function *)
; spec_pool : Specpool.t (** The spec pool *)
; hp_launch : Specpool.hp_launch (** The helping mechanism enablement *)
; seq_table : (Location.t, cprop) Hashtbl.t (** sequnential information *)
}
let ident_ABS = Id.create "ABS"
let ident_ABS_value = Id.create "ABS_value"
(** total number of iterations for all the calls to mk_stable_single *)
let stabilisation_iterations = ref 0
(** Checker for pure linearization points *)
let linear_pure_code = ref []
let udom_false = udom_of_uform_list []
let normalize_uforms_aggr =
List.reduce
(fun (p,sl) res ->
List.fold_append (fun p -> normalize_uform (p,sl))
(Pure.normalize_aggr p) res)
(** Return [true] if the correlation between the abstract state and
the concrete state been broken. *)
let linear_bad_invariant (p,sl) =
let (sl1,sl2) = List.partition
(function Csp_node(_,_,i,_) -> i == E.id ident_ABS | _ -> false)
sl in
let sl1_fv = List.fold
(fun sp r -> match sp with Csp_node(_,_,_,fld) ->
Fld.fold (fun t e r -> if t == Misc.list_data_tag then E.exfv e r else r) fld r | _ -> r)
sl1 IdSet.empty in
let sl2_fv = spat_fold E.exfv sl2 IdSet.empty in
not (IdSet.subset sl1_fv sl2_fv)
let linear_abs_pre =
(Pure.ptrue, [Csp_node(tag_default, node_component, E.id ident_ABS,
Fld.one Misc.list_data_tag (E.id ident_ABS_value))])
let str_is_fair x = Str.string_match (Str.regexp_string "fair") x 0
let str_is_cutpoint x = (x = "cutpoint")
let cutpoint_counter = ref 0
let next_cutpoint () =
incr cutpoint_counter;
"CUTPOINT_" ^ string_of_int (!cutpoint_counter)
(** Given an eprop, expose [e|->_] in each disjunct. *)
let ext_expose_ptsto prover e ep =
ext_transform
(fun cf -> prover.expose_ptsto (cprop_cform cf) e)
ep
(** Put [ep] into normal form *)
let ext_normalize prover ep =
ext_transform
(fun cf -> prover.nf_cprop [] (cprop_cform cf))
ep
(** Compute [er] such that [ep |- cq * er] *)
let ext_subtract prover ep cq =
ext_transform
(fun cf -> prover.find_frame_cprop [] (cprop_cform cf) cq)
ep
(** Compute [cr] such that [ep |- eq * cr] *)
let ext_ext_subtract prover ep eq =
let rec go l cf = match l with
| [] -> raise No_frame_found
| x::xl ->
let cp1 = cprop_cform (cform_of_eform cf) in
let cp2 = cprop_cform (cform_of_eform x) in
try
let res = prover.find_frame_cprop [] cp1 cp2 in
put_edge_skip(*TODO*) cf x;
res
with No_frame_found -> go xl cf in
aggr_remove_cform_duplicates
(List.reduce_append (go eq) ep)
(** Calculate postcondition after executing a generic command *)
let execute_gen_cmd prover (modif,cp,cq,s',loc) epre =
let epre = ext_append_assign (IdSet.fold (fun x r -> (x,None)::r) modif []) epre in
let sub_modif = mk_gensym_garb_subst_idset modif in
let fr =
try ext_subtract prover epre cp
with No_frame_found -> error_noframe_ext loc s' epre cp in
(if !verbose >= 6 then
print loc "FRAME inferred:@.@[<hov 2>%a@]@." pp_eprop fr);
cq @@*** map_eprop sub_modif fr
(** find the pure part of a proposition *)
let pure_part ep =
(*let intersection pl pl' = Pure.filter (fun ca -> mem_atom ca pl) pl' in *)
let rec go = function
| [] -> Pure.ptrue
| [n] -> fst (fst (cform_of_eform n))
| n::cfl -> Pure.ptrue (*intersection pl (go cfl)*) in
go ep
(** Simple symbolic execution for pure linearization checkers & eff. specs *)
let rec linear_symbexe prover c vars ufl = match c with
| [] ->
let sub = mk_gensym_garb_subst_idset vars in
List.reduce_append (map_uform sub) ufl
| c0 :: c -> begin match c0.can_st_desc with
| Cst_nondet (c1,c2) ->
linear_symbexe prover (c1 @ c) vars ufl
@ linear_symbexe prover (c2 @ c) vars ufl
| Cst_kill ids ->
let sub = mk_gensym_garb_subst_idset ids in
let ufl = List.reduce_append (map_uform sub) ufl in
linear_symbexe prover c (IdSet.diff vars ids) ufl
| Cst_assign (x,e) ->
let sub = mk_gensym_garb_subst x in
let eq = E.eq (E.id x) (sub e) in
let ufl = List.reduce
(fun uf res -> List.fold_append
(fun (p,sl) -> normalize_uform (eq @& p,sl))
(map_uform sub uf) res) ufl in
linear_symbexe prover c (IdSet.add x vars) ufl
| Cst_fldlookup (_rgnl,x,e,t) ->
let ufl = List.reduce
(fun (p,sl) res ->
let sub = mk_gensym_garb_subst x in
let e = Pure.to_sub p e in
try
let (cel,_) = prover.find_ptsto node_component e sl in
let eq = E.eq (E.id x) (sub (Fld.get t cel)) in
List.fold (fun uf res -> List.fold_append
(fun (p,sl) -> normalize_uform (eq @& p,sl))
(map_uform sub uf) res)
ufl res
with Not_found -> List.fold_append (map_uform sub) ufl res)
ufl in
linear_symbexe prover c (IdSet.add x vars) ufl
| Cst_assume cp ->
let ufl = List.reduce
(fun ((p_new,_),_) res -> List.fold
(fun (p,sl) res ->
List.fold_append (fun p -> normalize_uform (p,sl))
(Pure.normalize_aggr (Pure.conj p_new p))
res)
ufl res)
cp in
linear_symbexe prover c vars ufl
| Cst_assume_exp e ->
let p_new = Pure.one e in
let ufl = List.reduce
(fun (p,sl) res ->
List.fold_append (fun p -> normalize_uform (p,sl))
(Pure.normalize_aggr (Pure.conj p_new p))
res) ufl in
linear_symbexe prover c vars ufl
| Cst_fldassign (_rgnl,[(e1,t,e2)],_) ->
let ufl = List.reduce
(fun (p,sl) res ->
let e1 = Pure.to_sub p e1 in
try
let (cel,rest) = prover.find_ptsto node_component e1 sl in
let cel' = Fld.set t (Pure.to_sub p e2) cel in
(p, Csp_node (tag_default, node_component, e1, cel') :: rest) :: res
with Not_found -> pp_internal_error (); assert false (*TODO*))
ufl in
linear_symbexe prover c vars ufl
| Cst_assert_exp _
| Cst_fcall2 _ -> (*TODO---------------------------HACK_______________ *)
linear_symbexe prover c vars ufl
| Cst_fldassign _ | Cst_new _ | Cst_dispose _ | Cst_pfcall _
| Cst_action_begin _ | Cst_action_end _ | Cst_interfere _
| Cst_stabilize _ | Cst_loop _ | Cst_goto _ | Cst_comment _ ->
pp_internal_error ();
pp "Linear cmd: %a@." pp_cmd (c0::c);
assert false
end
(** Calculate post-condition outside block *)
let exit_from_block prover (rid,modif_body,cq0,loc) cq =
let rec remove_box rid =
ext_transform
(fun (uf,scpl) -> cprop_cform (uf, PList.remove_assq rid scpl)) in
let get_shared n cq_shared =
let cf = cform_of_eform n in
let fr = try PList.assq rid (snd cf)
with Not_found -> pp_internal_error (); assert false in
cprop_or cq_shared (and_cprop_pure (cprop_star fr cq0) (fst (fst cf))) in
let cq_local = (* local part of post-condition *)
try ext_subtract prover cq cq0
with No_frame_found -> error_noframe_ext loc "action exit" cq cq0 in
let cq_shared = List.reduce get_shared cq_local in
let cq_shared = and_cprop_pure cq_shared (pure_part cq_local) in
let sub = mk_gensym_garb_subst_idset modif_body in
let cq_local = remove_box rid cq_local in
let cq_local = map_eprop sub cq_local in
let cq = cprop_box rid cq_shared @@*** cq_local in
let cq =
let cq_local = List.map cform_of_eform cq_local in
let sub = mk_gensym_garb_subst_idset (prop_exfv cq_local IdSet.empty) in
map_eprop sub cq in
ext_normalize prover cq
(** A bogus assertion, used when abstraction raises [Junk]. *)
let junk_node =
cprop_spred
[Csp_node(tag_default,component_of_string "Junk",E.id Id.junk,Fld.emp)]
(* FIXME: this is a hack to avoid branches instead of the
straightforward [linear_symbexe prover (!linear_pure_code)].
*)
let exec_pure_lin_checker env =
match !linear_pure_code with [] -> identity | _::_ ->
List.reduce
(fun uf acc ->
if Pure.to_sub (fst uf) (E.id ident_lin_res) == E.undef then
let res =
linear_symbexe env.g_prover (!linear_pure_code) IdSet.empty [uf]
|> normalize_uforms_aggr
in
match res with [uf] -> uf :: acc
| [] -> acc
| (p,_)::ufl' ->
let pcomm = List.fold (fun (p,_) res -> Pure.common p res) ufl' p in
let (res_cr, res_o) =
List.partition (fun (p,_) -> Pure.has_can_return (Pure.simplify pcomm p)) res in
match res_cr, res_o with
| _::_, _::_ -> res@acc
| _ ->
(* pp "ex_p: %a@.all: %a@."
pp_cprop (cprop_pure pcomm)
pp_cprop (List.map (fun uf -> (uf,PNil)) res) ; *)
(Pure.conj pcomm (fst uf), snd uf) :: acc
else uf :: acc)
(** [make_stable cp rely] returns a [cp'] such that [cp |- cp'] and [stable_under cp rely] *)
let make_stable env cp actl =
let uform_list_to_cprop ufl = List.map (fun uf -> (uf,PNil)) ufl in
(** Pseudo-fix-point calculation for stability under a single action *)
let rec mk_stable_single act cou (udom, ufl_new) =
if ufl_new = [] || cou >= 4 then udom else begin
incr stabilisation_iterations;
let _ =
if !verbose >= 5 then
pp "interf %s@ new: %a@." (act_name act) pp_cprop (uform_list_to_cprop ufl_new)
else if !verbose >= 4 then
pp "interf %s@ new: %d@." (act_name act) (List.length ufl_new)
else ()
in
(* 1. Calculate effect of a single interference step *)
let ufl' =
ufl_new
|> uform_list_to_cprop
|> interfere_once env.g_prover act
|> List.map fst
|> normalize_uforms_aggr
|> exec_pure_lin_checker env
in
(* 2. Join *)
let res = env.g_abstraction.uform_join udom ufl' in
(* Fail quickly on unpromising lin. points *)
let _ = (* TODO ---------- *)
if (env.g_linear_pre != None) && List.exists linear_bad_invariant (snd res) then begin
if !verbose >= 1 then begin
pp "The current resource invariant looks unpromising for proving linearizability.@.";
List.iter (pp "AAA: %a@." pp_uform) ufl_new;
List.iter (pp "BBB: %a@." pp_uform) ufl';
List.iter (pp "CCC: %a@." pp_uform) (snd res);
List.iter (pp "BAD INV: %a@." pp_uform) (List.filter linear_bad_invariant (snd res));
end;
raise Symbolic_execution_error
end in
let _ =
if !verbose >= 5 then
pp "res: %a@." pp_cprop (uform_list_to_cprop (snd res))
in
(* 3. Repeat until fixed point *)
mk_stable_single act (cou + 1) res
end in
(** Fix-point calculation for stability under a list of actions *)
let rec mk_stable n (udom, ufl_new) =
if ufl_new = [] then udom else begin
let _ =
if !verbose >= 4 then begin
let ufl = uform_list_of_udom udom in
pp "go2(%d,%d,%d)@." n (List.length ufl)(List.length ufl_new);
if !verbose >= 5 then
pp "old: %a@ new: %a@."
pp_cprop (uform_list_to_cprop ufl)
pp_cprop (uform_list_to_cprop ufl_new)
end in
(uform_list_of_udom udom, []) (* TODO: Ugly -- breaks module abstraction!!! *)
|> List.fold (fun act udom -> mk_stable_single act 0 (udom, ufl_new)) actl
(* Stabilize each action separately *)
|> uform_list_of_udom
|> env.g_abstraction.uform_join udom (* Join with existing domain *)
|> mk_stable (n+1) (* Repeat until fixpoint *)
end in
(if !verbose >= 5 then pp "make_stable @ %a@." pp_cprop cp);
try
cp
|> aggr_kill_garbage_vars (* Turn useless vars into existentials *)
|> env.g_prover.nf_cprop []
|> List.map fst
|> normalize_uforms_aggr
(* |> exec_pure_lin_checker env *)
|> env.g_abstraction.uform_join udom_false (* Do an initial abstraction *)
|> mk_stable 0 (* Calculate fix-point *)
|> uform_list_of_udom
|> uform_list_to_cprop
with Junk -> junk_node
(** computes the fixpoint of a transformation from propositions to
propositions, such as the symbolic execution function *)
let compute_transf_fixpoint env (transf: eprop -> eprop) ep =
let rec fix ep_total ep ep_new =
if ep_new = [] then ep
else
let ep_new = transf ep in
let (ep_total,ep,ep_new) = env.g_abstraction.prop_join ep_total ep ep_new in
let _ = if !verbose >= 3 then pp "@.LOOP ADDING:@.%a@." pp_eprop ep_new in
fix ep_total ep ep_new
in
try
(* 1. Do an initial abstraction *)
(* This step is optional: abstracts the initial value.
Intuitively it should speed up the analysis slightly.
In practice, it does not affect performance in the 3 list algorithms. *)
let ep = env.g_abstraction.prop_abs ep in
let _ = if !verbose >= 3 then pp "@.LOOP STARTING:@.%a@." pp_eprop ep in
(* 2. Calculate fix-point *)
let pfix = fix ep ep ep in
let _ =
if !verbose >= 2 && not (Genarith.enabled ()) then
if env.g_no_interf_hack then
pp "@.LOOP NO-INTERFERENCE INV:@.%a@." pp_eprop pfix
else
pp "@.FOUND LOOP INVARIANT:@.%a@." pp_eprop pfix in
pfix
with
Junk -> eprop_of_cprop junk_node
(** computes the fixpoint of a transformation from propositions to
propositions using user provided qualifiers only *)
(*let compute_transf_qs_fixpoint env (transf: eprop -> eprop) ep rs qs =
let rtb = Hashtbl.create 16 in
let _ = List.iter (fun r -> Hashtbl.add rtb r qs) rs in
(* From qs to cprop *)
let cprop_of_qs qs =
List.fold_left (fun res q -> cprop_star res (cprop_cform q)) Assertions.cprop_empty qs in
(* Carefully add candidate invariants *)
let init_inv cp rtb =
let add_inv rid qs ((uf,scpl) as cf) =
if PList.mem_assq rid scpl then cf
else (uf, PCons (rid, cprop_of_qs qs, scpl)) in
ext_transform (fun cf -> [Hashtbl.fold add_inv rtb cf]) cp in
let rec fix rtb =
(* modify ep to add resource candidate inv *)
let ep = init_inv ep rtb in
let ep_new = transf ep in
(*let ep_new = env.g_abstraction.prop_abs ep_new in*)
let _ = pp "@.Begin eliminating...@." in
let rtb' = Qualifier.eliminate1 env.g_prover rtb ep_new in
let _ = pp "@.End eliminating...@." in
if (Qualifier.compare rtb rtb') then rtb
else fix rtb'
in
try
(* 1. Do an initial abstraction *)
(* This step is optional: abstracts the initial value.
Intuitively it should speed up the analysis slightly.
In practice, it does not affect performance in the 3 list algorithms. *)
let ep = env.g_abstraction.prop_abs ep in
let _ = if !verbose >= 3 then pp "@.LOOP STARTING:@.%a@." pp_eprop ep in
(* 2. Calculate fix-point *)
let pfix = init_inv ep (fix rtb) in
let _ =
if !verbose >= 2 && not (Genarith.enabled ()) then
if env.g_no_interf_hack then
pp "@.LOOP NO-INTERFERENCE INV:@.%a@." pp_eprop pfix
else
pp "@.FOUND LOOP INVARIANT:@.%a@." pp_eprop pfix in
pfix
with
Junk -> eprop_of_cprop junk_node*)
(** Compute [eq] such that [ep |- eq] and [stable_under ep rely] *)
let stabilize env (rid,rely) ep =
let get_shared rid (uf,scpl) =
try
((uf, PList.remove_assq rid scpl), PList.assq rid scpl)
with Not_found -> pp_internal_error (); assert false
in
let ep =
let cp = List.map cform_of_eform ep in
map_eprop (existentials_rename_sub (prop_exfv cp IdSet.empty)) ep
in
let eq = (* post-condition outside block *)
ext_transform (fun (cf : cform) ->
let (cf_local,cp_shared) = get_shared rid cf in
let (sub_unex,sub_toex) = existentials_rename_tonormal_sub (form_exfv cf_local IdSet.empty) in
let cp = map_cform sub_unex cf_local in
let cp_2 = map_cform sub_unex ((Pure.ptrue,snd(fst cf_local)),PNil) in
let cp_shared =
try map_cprop sub_toex (env.g_prover.find_frame_cprop [] (cprop_star cp cp_shared) cp_2)
with No_frame_found ->
pp_internal_error ();
pp "cp_shared: %a@." pp_cprop cp_shared;
pp "cf_local: %a@." pp_cform cf_local;
assert false
in
let cp_shared = make_stable env cp_shared rely in
cprop_cform (fst cf_local, PCons (rid, cp_shared, snd cf_local))) ep
in
(if !verbose >= 5 then
pp "Stabilisation result:@ %a@." pp_eprop eq);
eq
(** Hack to work around awkward semantics of [e|->fld]. *)
let all_fields = ref StringSet.empty
let populate_fields fld =
let rec go s fld =
let s = component_of_string s in
if Fld.hasfld s fld then fld
else Fld.set s (E.id (Id.gensym_str_ex (string_of_component s))) fld in
StringSet.fold go !all_fields fld
(* -------------------------------------------------------------------------- *)
(** {2 Action abstraction} *)
(* -------------------------------------------------------------------------- *)
let actabs_ids = idpool_new Id.gensym_str "!a"
let unify_spred inst sp1 sp2 = match sp1, sp2 with
| Csp_node (_,s1,e1,cel1), Csp_node (_,s2,e2,cel2) ->
if s1 <> s2 then None else
let inst = Fld.subset cel1 cel2 @& E.eq e1 e2 @& inst in
if Pure.is_false inst || Pure.has_unsat_eq inst then None else
Some inst
| Csp_listsegi (_,SINGLE (s1,fld1),e1,e2,e3,_,_,_), Csp_listsegi (_,SINGLE (s2,fld2),f1,f2,f3,_,_,_) ->
if s1 <> s2 then None else
let inst = Fld.subset fld1 fld2 @& E.eq e1 f1 @& E.eq e2 f2 @& E.eq e3 f3 @& inst in
if Pure.is_false inst || Pure.has_unsat_eq inst then None else
Some inst
| _ -> None
let unify_spatial inst sl1 sl2 =
let rec do_insert y xl rev_prefix res = match xl with
| [] -> List.rev_append rev_prefix [y] :: res
| x::xl' -> do_insert y xl' (x :: rev_prefix) (List.rev_append rev_prefix (y::xl) :: res) in
let rec gen_cases xl = match xl with
| [] -> [[]]
| x::xl -> List.fold_left (fun res l -> do_insert x l [] res) [] (gen_cases xl) in
let rec find_first f xl = match xl with
| [] -> None
| x::xl -> match f x with None -> find_first f xl | res -> res in
let rec easy_unify inst sl1 sl2 = match sl1, sl2 with
| [], [] -> Some inst
| sp1::sl1, sp2::sl2 ->
unify_spred inst sp1 sp2 >>= fun inst ->
easy_unify inst sl1 sl2
| _ -> None
in
find_first (easy_unify inst sl1) (gen_cases sl2)
let action_newname =
let n = ref 0 in
fun () -> incr n; "inferred_" ^ string_of_int !n
(** [action_subaction act1 act2 = Some inst] iff [act1] is a subaction
of [act2].
*)
let action_subaction prover sub_back0
(_name1,p1,sl_ctx1,sl_pre1,sl_post1)
(_name2,p2,sl_ctx2,sl_pre2,sl_post2) =
(* 1. Fail quickly on unpromising cases *)
if List.length sl_pre1 != List.length sl_pre2 then None
else if List.length sl_post1 != List.length sl_post2 then None
else
let (sub, sub_back) =
idpool_combine2 actabs_ids
(List.fold spred_exfv sl_ctx1
(List.fold spred_exfv sl_pre1
(List.fold spred_exfv sl_post1
(Pure.exfv p1 IdSet.empty))))
in
let p1 = Pure.map sub p1 in
let sl_ctx1 = map_spat sub sl_ctx1 in
let sl_pre1 = map_spat sub sl_pre1 in
let sl_post1 = map_spat sub sl_post1 in
(*TODO!!!!!!!!!!!!!!*)
unify_spatial Pure.ptrue sl_pre1 sl_pre2 >>= fun inst ->
unify_spatial inst sl_post1 sl_post2 >>= fun inst ->
let rec go n m xs =
if n > m || n < 0 then []
else if n = m then [xs]
else match xs with
| [] -> assert false
| x::xs ->
go n (m-1) xs
@ List.map (fun y->x::y) (go (n-1) (m-1) xs)
in
let rec find_first f xl = match xl with
| [] -> None
| x::xl -> match f x with None -> find_first f xl | res -> res in
let x = find_first (unify_spatial inst sl_ctx2)
(go (List.length sl_ctx2) (List.length sl_ctx1) sl_ctx1)
in
match x with
| None ->
begin try
let cp2 = normalize_cform ((Pure.conj inst p2, sl_ctx2),PList.nil) in
(* let _ = pp "NONE %a@ |- %a@." pp_uform (p1, sl_ctx1) pp_cprop cp2 in *)
let res = prover.find_frame_cprop []
(cprop_uform (p1, sl_ctx1)) cp2
in
let res = List.map (fun ((p,_),_) -> ((p,[]),PNil)) res in
Some (map_cprop (sub_back >> sub_back0) res)
with No_frame_found -> None
end
| Some inst ->
begin try
let cp2 = normalize_cform ((Pure.conj inst p2, spat_empty),PList.nil) in
(* let _ = pp "SOME %a@ |- %a@." pp_uform (p1, sl_ctx1) pp_cprop cp2 in *)
let res = prover.find_frame_cprop []
(cprop_uform (p1, spat_empty)) cp2
in
let res = List.map (fun ((p,_),_) -> ((p,[]),PNil)) res in
Some (map_cprop (sub_back >> sub_back0) res)
with No_frame_found -> None
end
(* HACK -- disable join. Gives poor performance. *)
(*
let action_subaction prover act1 act2 =
action_subaction prover act1 act2 &&
action_subaction prover act2 act1
*)
(** Convert action to (pl,cr,cp,cq) format *)
let action_convert cp_ctx cp cq =
List.fold (fun ((p_ctx, sl_ctx), _) ->
List.fold (fun ((p_pre, sl_pre), _) ->
List.fold (fun ((p_post, sl_post), _) ->
let pl = Pure.normalize_aggr (Pure.conj p_ctx (Pure.conj p_pre p_post)) in
List.fold (fun p res -> (action_newname(),p,sl_ctx,sl_pre,sl_post)::res) pl
) cq) cp) cp_ctx []
(** Convert action into (cr,cp,cq) format *)
let action_deconvert (name,p,cr,cp,cq) =
let cr = cprop_spred cr in
let cp = cprop_uform (p,cp) in
let cq = cprop_spred cq in
new_acts name cr cp cq
(** Abstract action [(pl,cr,cp,cq)] *)
let action_abstract abstraction sub_params (name,pl,cr,cp,cq) =
let (pl,cr,cp,cq) =
let sub = Pure.to_sub pl >> sub_params in
(Pure.map sub_params (Pure.remove_eqs pl),
map_spat sub cr, map_spat sub cp, map_spat sub cq) in
let (pl,cr,cp,cq) =
let exfv = List.fold spred_exfv cp (List.fold spred_exfv cq IdSet.empty) in
let (sub_unex,sub_toex) = idpool_combine2 actabs_ids exfv in
let (pl,cr) = match abstraction.uform_abs true [(Pure.map sub_unex pl, map_spat sub_unex cr)] with
| [(pl,x)] -> (Pure.map sub_toex pl, map_spat sub_toex x)
| ufl ->
pp_internal_error ();
pp "+++ %a@." pp_uform (pl, cr);
pp "=== %a@." pp_uform (Pure.map sub_unex pl, map_spat sub_unex cr);
List.iter (pp "--- %a@." pp_uform) ufl;
assert false
in
let cr = List.filter (function Csp_listsegi (_,SINGLE _,_,Enum 0,_,_,_,_) -> false | _ -> true) cr in
let cr = List.map
(function
| Csp_listsegi (tag,SINGLE(snode,_),e1,e2,e3,e4,_,ds) ->
Csp_listsegi (tag,SINGLE(snode,Fld.emp),e1,e2,e3,e4,Cem_PE,Dset.emp)
| sp -> sp) cr
in
(pl,cr,cp,cq)
in
let (fvp, fvq) =
(List.fold spred_fv cp IdSet.empty,
List.fold spred_fv cq IdSet.empty) in
(* Heuristic for locking and unlocking actions -- context is empty. *)
let cr =
if IdSet.mem Id.tid fvp != IdSet.mem Id.tid fvq then
spat_empty
else cr
in
(* Simplify @list predicates *)
let (pl,cr,cp,cq) =
let ff = (** Get all list expressions *)
let exp_to_list e = match e with
| Efun(Sfn_list,el) -> el
| e -> [e]
in
let go_fld t e res =
if t == Misc.list_data_tag then exp_to_list e :: res
else res
in
let get_lval s res = match s with
| Csp_node(_,_,_,fld) -> Fld.fold go_fld fld res
| Csp_listsegi(_,SINGLE _,_,_,e,_,_,_) -> exp_to_list e :: res
| _ -> res
in
List.fold get_lval
in
let ell = (*ff cr*) (ff cp (ff cq [])) in
let sub = Abstraction.mk_abs_list_sub ell in
(Pure.map sub pl,map_spat sub cr, map_spat sub cp, map_spat sub cq)
in
(* Simplify @set predicates *)
let (pl,cr,cp,cq) =
let ff = (** Get all set expressions *)
let exp_to_list e = match e with
| Efun(Sfn_set,el) -> el
| Efun(Sfn_list,el) -> List.map (E.fun1 Sfn_set_of_list) el
| e -> [e]
in
let go_fld t e res =
if t == Misc.list_data_tag then exp_to_list e :: res
else res
in
let get_lval s res = match s with
| Csp_node(_,_,_,fld) -> Fld.fold go_fld fld res
| Csp_listsegi(_,SINGLE _,_,_,e,_,_,_) -> exp_to_list e :: res
| _ -> res
in
List.fold get_lval
in
let ell = (*ff cr*) (ff cp (ff cq [])) in
let sub = Abstraction.mk_abs_set_sub IdSet.empty ell in
(Pure.map sub pl,map_spat sub cr, map_spat sub cp, map_spat sub cq)
in
let (fvp, fvq) =
(List.fold spred_fv cp IdSet.empty,
List.fold spred_fv cq IdSet.empty) in
let pl =
let kills = IdSet.diff (Pure.exfv pl IdSet.empty)
(spat_fold E.exfv cr (IdSet.union fvp fvq))
in
let pl = Pure.kill_vars kills pl in
(* TODO: Figure out better heuristic... *)
let exfv2 = IdSet.filter Id.is_existential (IdSet.diff fvq fvp) in
let myf e =
let fv = E.exfv e IdSet.empty in
IdSet.is_empty fv
|| (match e with Efun1 (Sfn_NOT, Eeq(Enum 0,_)) -> true | _ -> false)
|| ((match e with Efun2 (Sfn_list_lt,_,_) -> true | _ -> false)
&& IdSet.exists (function x -> IdSet.mem x exfv2) fv)
in
Pure.filter myf pl
in
(name,pl,cr,cp,cq)
(** Join action act to the action set recorded in [env]. *)
let action_join env actlr sub_back rid act =
let insert_act actlr (s,_,_,_,_) inst =
let inst =
List.map (fun ((p,_),_) -> ((Pure.only_inst_eqs p,[]),PNil)) inst in
let (l, cp) =
try
let cp = List.assq s !actlr in
let l = List.remove_assq s !actlr in
(l, cp)
with Not_found -> (!actlr, cprop_false) in
actlr := (s, cprop_or inst cp) :: l in
let myf (r,act') =
if r == rid then
match action_subaction env.g_prover sub_back act act' with
| None -> true
| Some inst -> insert_act actlr act' inst; false
else true
in
let myg (r,act') = r != rid || (action_subaction env.g_prover identity act' act == None) in
if List.for_all myf env.g_guarantee then begin
let _ =
if !verbose >= 3 then begin
let (name,pl,cr,cp,cq) = act in
pp "Added action: %s %s@.@[<hv>%a@ | %a @ ~> %a@]@."
(string_of_component rid) name
pp_uform (pl, cr)
pp_uform (Pure.ptrue, cp)
pp_uform (Pure.ptrue, cq)
end
in
insert_act actlr act cprop_empty;
env.g_guarantee <- (rid,act) :: List.filter myg env.g_guarantee;
env.g_guar_changed <- true
end
(** Add action [cp_ctx | cp ~~> cq] to the guarantee. *)
let register_guarantee env actlr rid cp_ctx cp cq =
if !verbose >= 6 then begin
pp "register guarantee: %s@.@[<hv>%a@ | %a @ ~> %a@]@."
(string_of_component rid)
pp_cprop cp_ctx
pp_cprop cp
pp_cprop cq
end;
(* 1. Forget local variables *)
let (cp_ctx, cp, cq) =
let cp_ctx = prop_kill_can_return cp_ctx in
let cp = prop_kill_can_return cp in
let cq = prop_kill_can_return cq in
let fv = prop_fv cp_ctx (prop_fv cp (prop_fv cq IdSet.empty)) in
let locals = IdSet.diff (IdSet.diff fv env.g_globals) env.g_params in
let sub = mk_gensym_garb_subst_idset locals in
(map_cprop sub cp_ctx, map_cprop sub cp, map_cprop sub cq) in
(* Substitution for parameters *)
let (sub, sub_back) = mk_gensym_garb_subst_idset2 env.g_params in
(* 2. For each action... *)
List.iter
(action_abstract env.g_abstraction sub
>> action_join env actlr sub_back rid)
(action_convert cp_ctx cp cq)
let get_reachable froml sl =
let add x y = if List.exists (fun y -> equal_exp x y) y then y else x::y in
let add_reach_vars res sp = match sp with
| Csp_node (_,_,_,fld) -> Fld.fold_val add fld res
| Csp_listsegi(_,_,e,f,g,h,_,_) -> add e (add f (add g (add h res)))
| Csp_arr (_,e,f,g,_,_,_) -> add e (add f (add g res))
| Csp_indpred _ -> res in
let is_pred_reachable x sp = match sp with
| Csp_arr (_,e,_,_,_,_,_) (*TODO*)
| Csp_node (_,_,e,_) -> equal_exp x e
| Csp_listsegi(_,SINGLE _,e,_,_,_,_,_) -> equal_exp x e
| Csp_listsegi(_,(XOR _ | DOUBLE _),e1,_,e2,_,_,_) -> equal_exp x e1 || equal_exp x e2
| Csp_indpred _ -> false in
let rec go_reach seen todo sl1 sl2 = match todo with
| [] -> (sl1, sl2)
| x::todo ->
let (sl1new,sl2) = List.partition (is_pred_reachable x) sl2 in
let seen = x::seen in
let todo = List.fold_left add_reach_vars todo sl1new in
let todo = List.filter (fun x -> not (List.exists (fun y -> equal_exp x y) seen)) todo in
go_reach seen todo (sl1new @ sl1) sl2 in
go_reach [] froml [] sl
(** Helper function *)
let reduce_list f cfl =
let g reso cf =
reso >>= fun res ->
f cf >>= fun cfl -> Some (List.rev_append cfl res) in
List.fold_left g (Some []) cfl
(* -------------------------------------------------------------------------- *)
(** {2 Symbolic execution of field lookup and update} *)
(* -------------------------------------------------------------------------- *)
(** In the context [rctx], calculate the postcondition
of executing [x = e->t] given the precondition [cpre]. *)
let execute_fld_lookup prover rctx x e t cpre =
(* Old value of x is now garbage *)
let sub = mk_gensym_garb_subst x in
(* Read from cf *)
let rec go_simp e rctx ((pl2,sl2),scpl2) = (* type of return is cform list option or cprop option *)
let e = (Pure.to_sub pl2) e in
try
let (cel,sl2b) = prover.find_ptsto node_component e sl2 in
let (f,cel') = Fld.get_extend t cel in
let f' = sub f in
let cp = map_cform sub ((pl2,Csp_node(tag_default,node_component,e,cel')::sl2b),scpl2) in
Some (and_cprop_pure cp (Pure.one (E.eq (E.id x) f')))
with Not_found ->
go_ctx e rctx ((pl2,sl2),scpl2)
and go e rctx cf =
let cp = prover.expose_ptsto (cprop_cform cf) e in
reduce_list (go_simp e rctx) cp
and go_ctx e rctx ((pl2,sl2),scpl2) =
match rctx with
| [] -> None
| rid::rctx ->
try match reduce_list (go e []) (and_cprop_pure (PList.assq rid scpl2) pl2) with
| None -> go_ctx e rctx ((pl2,sl2),scpl2)
| Some cfl ->
let cp2 = map_cform sub ((pl2,sl2), PList.remove_assq rid scpl2) in
Some (List.map (fun (uf2, scpl2) -> (uf2, PCons (rid, cfl, scpl2))) cp2)
with Not_found -> go_ctx e rctx ((pl2,sl2),scpl2) in
let go_ext_simp e rctx n = (* type of go simple is (cform -> cform list option); type of n is eform *)
ext_opt_transform1 (go_simp e rctx) n in
let go_ext e rctx n =
ext_expose_ptsto prover e [n] (* return eprop *)
|> reduce_list (go_ext_simp e rctx) in
reduce_list (go_ext e rctx) cpre
(** In the context [rctx], calculate the postcondition
of executing [e1->t1 = f1, ... en->tn = fn] given the precondition [cpre]. *)
let execute_fld_assign env actlr rctx assignl cpre =
(* Deal with shared writes *)
let go_shared (rid : component) ((pl_local,sl_local),scpl) ((pl_shared,sl_shared),scpl') =
(* TODO :: Normalize cf_local * pl_shared ! *)
try
let (old_vals,new_vals,old_nodes,new_nodes,sl_rem_shared) =
let sub = Pure.to_sub pl_shared in
List.fold_left
(fun (e2_olds,e2s,old_nodes,new_nodes,sl_rem_shared) (e1,t,e2) ->
let e1 = sub e1 in
let e2 = sub e2 in
let (cel,sl_rem_shared) =
env.g_prover.find_ptsto node_component e1 sl_rem_shared in
let cel = populate_fields cel in
let (e2_olds, e2) = (* HACK -- abstraction for unlocking actions *)
match Fld.try_get t cel with
| Some e2_old ->
if e2 == E.zero && e2_old == E.tid then
(e2_old::e2_olds, E.id (Id.gensym_str_ex "unlock"))
else
(e2_old::e2_olds, e2)
| None -> (e2_olds, e2) in
let e2s = e2::e2s in
let old_nodes = Csp_node(tag_default,node_component,e1,cel)::old_nodes in
let new_nodes = Csp_node(tag_default,node_component,e1,Fld.set t e2 cel)::new_nodes in
(e2_olds,e2s,old_nodes,new_nodes,sl_rem_shared))
([],[],[],[],sl_shared) assignl
in
(* Ownership transfer: private -> shared *)
let (sl_transf_to_shared,sl_local) = get_reachable new_vals sl_local in
(* Ownership transfer: shared -> private *)
let (sl_transf_to_local,sl_rem_shared) =
if !allow_leaks then ([],sl_rem_shared)
else
let sl3 = spat_star new_nodes (spat_star sl_transf_to_shared sl_rem_shared) in
let (_,transf) = get_reachable (List.map E.id (IdSet.elements env.g_globals)) sl3 in
let (transf,_) = get_reachable old_vals transf in