-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathcheckproof.ml
1365 lines (1296 loc) · 59.7 KB
/
checkproof.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
(* This file is part of Arsenic, a proofchecker for New Lace logic.
Copyright (c) 2015-2016 Richard Bornat.
Licensed under the MIT license (sic): see LICENCE.txt or
https://opensource.org/licenses/MIT
*)
open Function
open Tuple
open Sourcepos
open Listutils
open Program
open Thread
open Com
open Knot
open Stitch
open Name
open Formula
open Graph
open Settings
open Labmap
open Order
open Node
open Report
open AskZ3
open Stability
open Intfdesc
open Location
exception Crash of string
exception ModalQFail (* internal, see below *)
let proofobs = ref 0
let notyet spos s = Printf.printf "\n\n** %s: not yet checking %s" (string_of_sourcepos spos) s
(* a type for reporting lo-parallel interference *)
type loparkind =
| InsideLo
| BeforeLo
| AfterLo
let string_of_loparkind = function
| InsideLo -> "inside"
| BeforeLo -> "before"
| AfterLo -> "after"
let report_z3result r spos stringfun =
match r with
| Valid _ -> ()
| Invalid _ -> report (Error (spos, ("we do not have " ^ stringfun())))
| Undecided _ -> report (Undecided (spos, ("Z3 cannot decide " ^ stringfun())))
| BadQuery (f,s) -> raise (Crash (Printf.sprintf "\n\n** BADQUERY ** %s: %s\n\ngenerates\n\n%s\n\n"
(string_of_sourcepos spos)
(string_of_formula f)
s
)
)
let assign_of_triplet ct =
match ct.tripletof.sc_node with
| Assign a -> a
| _ ->
raise (Invalid_argument ("Checkproof.assign_of_triplet " ^ string_of_triplet string_of_simplecom ct))
(* a map from pkind * simplecom triplet *)
let string_of_pkscmap_key = bracketed_string_of_pair
string_of_pkind
(string_of_triplet string_of_simplecom)
module PKSCMap = MyMap.Make (struct type t = pkind * simplecom triplet
let compare = Pervasives.compare
let to_string = string_of_pkscmap_key
end
)
(* precondition of each simplecom triplet. Different for load_reserved, store-conditional *)
(* let we_are_latest v = _recEqual (_recLatest Here NoHook v) (_recFname v) *)
let cpre go_sat pk ct =
let defaultpre = precondition_of_knot go_sat pk ct.tripletknot in
(* if Com.is_loadreserved ct then
(match defaultpre with
| PreSingle fpre -> defaultpre
| PreDouble (fpre, locs, _) -> report (Error (ct.tripletpos,
Printf.sprintf "precondition of load_reserved has %s"
(prefixed_phrase_of_list string_of_location
"reservation for" "reservations for"
locs
)
)
);
PreSingle fpre
)
else
if Com.is_storeconditional ct then
(let a = Com.assign ct in
let resloc = Assign.reserved a in
let resv = Location.locv resloc in
match defaultpre with
| PreSingle fpre ->
report (Error (ct.tripletpos,
Printf.sprintf "precondition of store-conditional has no reservation for %s"
(string_of_location resloc)
)
);
PreDouble (fpre,[resloc], conjoin [fpre; we_are_latest resv])
| PreDouble (fpre,locs,fpreres) ->
if not (List.exists (Location.eq resloc) locs) then
report (Error (ct.tripletpos,
Printf.sprintf "precondition of store-conditional has no reservation for %s"
(string_of_location resloc)
)
);
if List.length locs>1 then
report (Error (ct.tripletpos,
Printf.sprintf "precondition of store-conditional has %s"
(prefixed_phrase_of_list
string_of_location
"reservation for" "reservations for"
(List.filter (not <.> Location.eq resloc) locs)
)
)
);
PreDouble (fpre,[resloc],conjoin [fpreres; we_are_latest resv])
)
else defaultpre
*)
defaultpre
(* interference of each simplecom triplet, Elaboration and Interference (maybe I'll change those names back ...) *)
(* Even register assignments interfere, but (see condition in parser) they don't have interference pres *)
type intf = intfdesc (*
| IntfSingle of intfdesc
| IntfDouble of intfdesc * intfdesc (* normal, reserved *)
*)
let string_of_intf = string_of_intfdesc (* function
| IntfSingle i -> "IntfSingle(" ^ string_of_intfdesc i ^ ")"
| IntfDouble (i,ires) -> "IntfDouble((" ^ string_of_intfdesc i
^ "),("
^ string_of_intfdesc ires
^"))"
*)
let intf_fold f v = f v (* function
| IntfSingle i -> f v i
| IntfDouble (i,ires) -> f (f v ires) i
*)
let intf_iter f = intf_fold (fun () -> f) ()
let mkintf cpre pk ct =
let assign = assign_of_triplet ct in
let preopt = ct.tripletof.sc_ipreopt in
let defaultpre = cpre Interference ct in
let intfdesc fpre = Intfdesc.mk_intfdesc ct.tripletpos fpre assign in
(* if Assign.is_loadreserved assign then
(let fpre, fpreres =
match defaultpre with
| PreSingle fpre -> fpre, conjoin [fpre; we_are_latest (Location.locv (Assign.reserved assign))]
| _ ->
raise (Crash (Printf.sprintf "%s %s has double pre %s"
(string_of_sourcepos ct.tripletpos)
(string_of_triplet string_of_simplecom ct)
(string_of_pre defaultpre)
)
)
in
IntfDouble (intfdesc fpre, intfdesc fpreres)
)
else
if Assign.is_storeconditional assign then
(let fpreres =
match defaultpre with
| PreDouble (_,_,fpreres) -> fpreres
| _ ->
raise (Crash (Printf.sprintf "%s %s has single pre %s"
(string_of_sourcepos ct.tripletpos)
(string_of_triplet string_of_simplecom ct)
(string_of_pre defaultpre)
)
)
in
match preopt with
| None -> IntfSingle (intfdesc fpreres)
| Some (IpreRes fpreres) -> IntfSingle (intfdesc fpreres)
| Some (IpreSimple fpre) ->
report (Error (ct.tripletpos,
"store-conditional does not need an unreserved-interference precondition"
)
);
IntfSingle (intfdesc fpreres)
| Some (IpreDouble(_,fpreres)) ->
report (Error (ct.tripletpos,
"store-conditional does not need an unreserved-interference precondition"
)
);
IntfSingle (intfdesc fpreres)
)
else (* just an ordinary assignment *)
((* check it doesn't assign to its own reservation *)
(match Assign.is_var_assign assign, defaultpre with
| true , PreDouble(_,locs,_) ->
let alocs = fstof2 (List.split (Assign.loces assign)) in
let badlocs = List.filter (fun aloc -> List.mem aloc locs) alocs in
if badlocs<>[] then
report (Error (ct.tripletpos,
Printf.sprintf "precondition has %s; but it assigns to %s"
(prefixed_phrase_of_list
string_of_location
"reservation" "reservations"
alocs
)
(standard_phrase_of_list string_of_location badlocs)
)
)
| _ -> ()
);
match preopt with
| None ->
(match defaultpre with
| PreSingle pre -> IntfSingle (intfdesc pre)
| PreDouble (pre,_,preres) -> IntfDouble (intfdesc pre, intfdesc preres)
)
| Some (IpreSimple pre) ->
(match defaultpre with
| PreSingle _ -> IntfSingle (intfdesc pre)
| PreDouble (_,_,preres) -> IntfDouble (intfdesc pre, intfdesc preres)
)
| Some (IpreRes preres) ->
(match defaultpre with
| PreSingle pre -> IntfDouble (intfdesc pre, intfdesc preres)
| PreDouble (pre,_,_) -> IntfDouble (intfdesc pre, intfdesc preres)
)
| Some (IpreDouble (pre,preres)) -> IntfDouble (intfdesc pre, intfdesc preres)
)
*)
intfdesc (match preopt with
| None -> defaultpre
| Some pre -> pre
)
(* postconditions of each simplecom triplet *)
type post = formula (*
| PostSingle of formula
| PostDouble of formula * location * formula (* unreserved, reservation, reserved *)
*)
let string_of_post = string_of_formula (* function
| PostSingle f -> "IntfSingle(" ^ string_of_formula f ^ ")"
| PostDouble (f,loc,fres) -> "PostDouble((" ^ string_of_formula f
^ "),"
^ string_of_location loc
^ ",("
^ string_of_formula fres
^"))"
*)
(* floc has to deliver a single location ... *)
let post_of_pre fpre (* floc *) pre = fpre pre (*
match pre with
| PreSingle pre -> PostSingle (fpre pre)
| PreDouble (pre, locs, preres) -> PostDouble (fpre pre, floc locs, fpre preres)
*)
(* let justoneloc pos = function
| [] -> raise (Crash (Printf.sprintf "%s justoneloc no locs" (string_of_sourcepos pos)))
| [loc] -> loc
| loc::_ as locs ->
report (Error (pos,
Printf.sprintf "precondition has more than one location reservation: %s"
(standard_phrase_of_list string_of_location locs)
)
);
loc
*)
let cpost cpre pk ct =
let pre = cpre pk ct in
match ct.tripletof.sc_node with
| Skip -> post_of_pre id (* (justoneloc ct.tripletpos) *) pre
| Assert f -> post_of_pre (fun pre -> conjoin [pre; f]) (* (justoneloc ct.tripletpos) *) pre
| Assign a ->
let apost pre =
post_of_pre (fun pre -> Strongestpost.strongest_post true pre a) (* (justoneloc ct.tripletpos) *) pre
in
(* if Assign.is_loadreserved a then
(match pre with
| PreSingle fpre ->
let resloc = Assign.reserved a in
let pre = PreDouble (fpre, [resloc], conjoin [fpre; we_are_latest (Location.locv resloc)]) in
apost pre
| _ ->
raise (Crash (Printf.sprintf "%s %s has double pre %s"
(string_of_sourcepos ct.tripletpos)
(string_of_triplet string_of_simplecom ct)
(string_of_pre pre)
)
)
)
else
if Assign.is_storeconditional a then
(* add 'latest' to pre and postcondition *)
let resloc = Assign.reserved a in
let resv = Location.locv resloc in
let latest_after = _recEqual (_recLatest Here NoHook resv) (Assign.conditionally_stored a) in
post_of_pre (fun fpre -> conjoin [Strongestpost.strongest_post true (conjoin [fpre; we_are_latest resv]) a; latest_after])
(justoneloc ct.tripletpos)
pre
else
*)
apost pre
type z3query = z3question * bool * (unit -> string) * formula * formula list
type z3key = z3question * formula * formula list
let z3key_of_z3query (q,_,_,a,gs) = q, Formula.stripspos a, List.map Formula.stripspos gs
let string_of_z3key (q,a,gs) =
Printf.sprintf "%s %s %s"
(string_of_z3question q)
(string_of_formula a)
(bracketed_string_of_list string_of_formula gs)
(* to use this map, apply z3key_of_z3query to a z3query *)
module Z3Map = MyMap.Make (struct type t = z3key
let compare = Pervasives.compare
let to_string = string_of_z3key
end
)
type onode = order * node
let string_of_onode (o,n) = Printf.sprintf "%s %s" (string_of_order o) (string_of_node n)
let checkproof_thread check_taut ask_taut ask_sat avoided
preopt postopt givopt nintfs
threadnum knotmap labmap opgraph
thread =
Thread.threadnum := threadnum;
if !verbose then
Printf.printf "\nstarting thread %d" threadnum;
let go_sat loc ipre =
let stringfun () = Printf.sprintf "checking satisfiability of interference pre (includes go constraint) %s"
(string_of_formula ipre)
in
match ask_sat loc stringfun ipre with
| Invalid _ -> false (* unsatisfiable *)
| _ -> true (* satisfiable or undecided *)
in
let cpre_of_ct =
curry2 (PKSCMap.vmemofun !verbose "cpre"
string_of_pkscmap_key
string_of_pre
id
(uncurry2 (cpre go_sat))
)
in
let intf_of_ct =
curry2 (PKSCMap.vmemofun !verbose "intfdesc"
string_of_pkscmap_key
string_of_intf
id
(uncurry2 (mkintf cpre_of_ct))
)
in
let cpost_of_ct =
curry2 (PKSCMap.vmemofun !verbose "cpost"
string_of_pkscmap_key
string_of_post
id
(uncurry2 (cpost cpre_of_ct))
)
in
let sourcepost_of_stitch pk stitch =
let order = order_of_stitch stitch in
let source = source_of_stitch stitch in
let lab = label_of_node source in
let cid = get_cid lab labmap in
let post =
match cid with
| CidSimplecom ct -> cpost_of_ct pk ct
| CidControl c ->
(match source with
| CEnode (_,b) ->
(match c with
| CExpr ft -> let pre = precondition_of_knot go_sat pk ft.tripletknot in
post_of_pre
(fun pre -> conjoin [pre; (if b then ft.tripletof else _recNot (ft.tripletof))])
(* (justoneloc ft.tripletpos) *)
pre
| CAssign ct -> (match b, cpre_of_ct pk ct with
(* | false, PreDouble (pre, _, _) -> PostSingle pre *)
| false, (* PreSingle *) (pre) ->
report (Error (ct.tripletpos, "store-conditional has no reserved constraint"));
(* PostSingle *) pre
(* | true , PreDouble _ ->
(match cpost_of_ct pk ct with
| PostDouble (_,_,postres) -> PostSingle postres (* I think *)
| _ ->
raise (Crash (string_of_sourcepos ct.tripletpos
^ " sourcepost_of_stitch only one post"
)
)
)
*)
| true , (* PreSingle *) (pre) ->
report (Error (ct.tripletpos, "store-conditional has no reserved constraint"));
cpost_of_ct pk ct
)
)
| _ ->
raise (Crash (Printf.sprintf "%s Checkproof.sourcepost_of_stitch %s %s %s %s"
(string_of_sourcepos stitch.stitchpos)
(string_of_order order)
(string_of_pkind pk)
(string_of_node source)
(string_of_labelid (LabMap.find lab labmap))
)
)
)
| CidInit (_,f) -> (* PostSingle *) (sofar NoHook f) (* used to have (universal NoHook f) *)
| CidThreadPost _
| CidFinal _ ->
raise (Crash (Printf.sprintf "%s: stitch %s refers to thread/program postcondition"
(string_of_sourcepos (pos_of_stitch stitch))
(string_of_stitch stitch)
)
)
in
let spopt = spopt_of_stitch stitch in
(* (* this thing is only called once: we can check the arity here *)
(match post, spopt with
| PostSingle _, Some (SpostDouble _)
| PostSingle _, Some (SpostRes _) ->
report (Error (stitch.stitchpos,
Printf.sprintf "constraint source %s cannot generate a reservation postcondition"
(label_of_node stitch.stitchsource)
)
)
| _ -> ()
);
*)
post, spopt
in
let intf_from (i,_) =
if i<0 then "rely" else ("thread " ^ string_of_int i)
in
let check_external_stability spos (* locopt *) assertion (_,intfdesc as intf) =
(* let resopt = locopt in *)
let stringfun stabkind () =
Printf.sprintf "%s of %s against %s (from %s)"
stabkind
(string_of_formula assertion)
(string_of_intfdesc intfdesc)
(intf_from intf)
(* (match resopt with
| Some loc -> Printf.sprintf " (disregarding interference with %s)"
(string_of_location loc)
| None -> ""
)
*)
in
let assigned = Intfdesc.assigned intfdesc in
let frees = Formula.frees assertion in
if NameSet.is_empty (NameSet.inter assigned frees) then
avoided spos "" (stringfun "external stability check")
else
(let extq = Stability.ext_stable_query_intfdesc assertion intfdesc in
check_taut spos (stringfun "EXT stability") extq;
if not (Formula.exists (is_recU <||> is_recSofar (* <||> is_recLatest *)) assertion) then
avoided spos "Z3 check" (stringfun "UEXT stability")
else
(let uextq = Stability.uext_stable_query_intfdesc assertion intfdesc in
check_taut spos (stringfun "UEXT stability") uextq
)
)
in
(* check inclusion of interference in guarantee, rely *)
let check_intf_included kindstring intfdesc rgs =
let allfrees =
List.fold_left NameSet.union NameSet.empty (List.map Intfdesc.frees (intfdesc::rgs))
in
let freevs = NameSet.filter Name.is_anyvar allfrees in
let newforold v = Name.var_of_string (string_of_var v ^ "&new") in
let tranloce (loc,e) =
match loc with
| VarLoc v -> _recEqual (_recFname (newforold v)) e
in
let tranloces = conjoin <.> List.map tranloce in
let tranextravs =
conjoin
<.> List.map (fun v -> _recEqual (_recFname (newforold v)) (_recFname v))
<.> NameSet.elements
in
let translate intfdesc =
let pre = Intfdesc.pre intfdesc in
let loces = Intfdesc.loces intfdesc in
let locs,_ = List.split loces in
let extravs = NameSet.diff freevs (NameSet.of_list (List.map Location.locv locs)) in
conjoin [pre; tranloces loces; tranextravs extravs]
in
let tranrg intfdesc =
let f = translate intfdesc in
bindExists (Intfdesc.binders intfdesc) f
in
(* (* if it's a normal assign, don't look at storeconditionals in rgs *)
let normal intfdesc = not (Assign.is_storeconditional (Intfdesc.assign intfdesc)) in
let rgs =
if normal intfdesc then List.filter normal rgs else rgs
in
*)
let query = _recImplies (translate intfdesc)
(disjoin (tranextravs freevs :: List.map tranrg rgs))
in
let stringfun () = Printf.sprintf "inclusion of %s in %s"
(string_of_intfdesc intfdesc)
kindstring
(* (Listutils.bracketed_string_of_list string_of_intfdesc rgs) *)
in
check_taut intfdesc.ipos stringfun query
in
(* a constraint b->c is lo-interfered with by an assign a if there is an so-tree path
containing (instances of) a, b and c which can be reordered so that a comes between
b and c. In the proof checker this means that either
1. There is an so path b..c which includes a.
(In the cause of minimalism, a path which remains within the tightest
loop that encloses b and c); or
2. a is not b or c and there is an so path a->b but no lo path which follows
that so path (i.e. doesn't visit nodes outside it); or
3. a is not b or c and there is an so path c->a which follows that so path.
*)
let get_parents lab = Labmap.get_parents lab labmap in
(* take an opset; find paths which are so without a corresponding path
which satisfies order_filter (checking for lo, bo or uo as appropriate)
*)
let so_butnot_constraint order_filter opset =
let okpath (_,_,soset as so) (_,_,cset as lo) =
let r = NodeSet.is_empty (NodeSet.diff cset soset) in
if !verbose then
Printf.printf "\nso=%s; lo=%s; diff=%s"
(string_of_opath so) (string_of_opath lo)
(NodeSet.to_string (NodeSet.diff cset soset));
r
in
OPSet.filter
(fun path -> is_so_opath path &&
not (OPSet.exists (fun cpath -> order_filter cpath &&
okpath path cpath
)
opset
)
)
opset
in
let rec check_knot clab rely assigns inneropt knot =
let cnode = Cnode clab in
if !verbose || !Settings.verbose_knots then
Printf.printf "\n%s: checking knot %s inneropt %s"
(string_of_sourcepos knot.knotloc)
(string_of_knot knot)
(Option.string_of_option OPSet.to_string inneropt);
let cstitch inneropt () stitch =
if !verbose || !Settings.verbose_knots then
Printf.printf "\n -- looking at stitch %s inneropt %s"
(string_of_stitch stitch)
(Option.string_of_option OPSet.to_string inneropt);
let bnode = source_of_stitch stitch in
let blab = label_of_node bnode in
let bassert = assertion_of_stitch stitch in
if !verbose || !Settings.verbose_knots then
Printf.printf "\nexamining constraint %s->%s" (string_of_node bnode) (string_of_node cnode);
(* inheritance of stitch -- we do Interference -> Interference. Hmm. *)
(* inheritance on bo is tricky: we would like to do _B(sourcepost) => embroidery.
When sourcepost is subst_clean (no enhat or hooked subformulas), that's ok.
If embroidery is _B(P), just do sourcepost=>P. If embroidery is a conjunction,
do it piecewise. If it's forall x (B(P)), treat as B(forall x P). But otherwise
we're riding for a fall.
The same applies, mutatis mutandis, to _U.
If it turns out to be a problem, we could have a syntax to allow the user to
say what sourcepost should be, check that's implied by the actual sourcepost,
and then do _B/_U(sourcepost) => embroidery.
*)
let modalq sourcenode sourcepost is_modal wrap_modal embroidery =
let modal_free = not <.> Formula.exists (Option.bool_of_opt <.> is_modal) in
let is_const f = NameSet.cardinal (NameSet.filter Name.is_anyvar (Formula.frees f)) = 0 in
let rec mq e =
match is_modal e with
| Some prop -> prop
| None ->
if modal_free e then e else
(match deconjoin e with
| Some es -> conjoin (List.map mq es)
| None -> (* not conjoined *)
(match dedisjoin e with
| Some es -> if List.length (List.filter (not <.> is_const) es) <= 1
then disjoin (List.map mq es)
else raise ModalQFail
| None -> (* not conjoined, not disjoined *)
(match e.fnode with
| Binder(Forall,_,_) ->
let ns, eb = multibind Forall [] e in
(match is_modal eb with
| Some prop -> bindForall (NameSet.of_list ns) prop
| None -> raise ModalQFail
)
| _ -> (* not conjoined, not disjoined, not forall *)
raise ModalQFail
)
)
)
in
try let prop = mq embroidery in _recImplies sourcepost prop
with ModalQFail ->
if subst_clean sourcepost then
_recImplies (wrap_modal sourcepost) embroidery
else
(report
(Error(pos_of_stitch stitch,
Printf.sprintf "Arsenic cannot guess R such that strongest-post(%s)=>R \
and %s=>%s. \
(Fix this problem by including R, in assertion braces, \
between '%s' and ':')"
(string_of_formula sourcepost)
(string_of_formula (wrap_modal (_recFname "R")))
(string_of_formula embroidery)
(Node.string_of_node sourcenode)
)
);
_recTrue
)
in
let order = order_of_stitch stitch in
let sourcenode = source_of_stitch stitch in
let sourcepost, spopt =
match order with
| So -> raise (Crash (Printf.sprintf "so in knot %s" (string_of_knot knot)))
| _ -> sourcepost_of_stitch Elaboration stitch (* Elaboration always, even with go *)
in
let sourcepost =
match spopt with
| None -> sourcepost
| Some spost -> spost
(* | Some (SpostSimple post) ->
(match sourcepost with
| PostSingle _ -> PostSingle post
| PostDouble (_,loc,postres) -> PostDouble (post, loc, postres)
)
| Some (SpostRes postres) ->
(match sourcepost with
| PostSingle post ->
report (Error (stitch.stitchpos,
Printf.sprintf "stitch source %s does not have a \
reserved postcondition, yet stitch \
has a reserved precondition"
blab
)
);
PostDouble (post, VarLoc "??", postres)
| PostDouble (post,loc,_) -> PostDouble (post, loc, postres)
)
| Some (SpostDouble (post, postres)) ->
(match sourcepost with
| PostSingle _ ->
report (Error (stitch.stitchpos,
Printf.sprintf "stitch source %s does not have a \
reserved postcondition, yet stitch \
has a reserved precondition"
blab
)
);
PostDouble (post, VarLoc "??", postres)
| PostDouble (_,loc,_) -> PostDouble (post, loc, postres)
)
in
let sourcepost = post
match is_reserved_stitch stitch, sourcepost with
| _ , PostSingle post -> post
| true , PostDouble (_ , _, postres) -> postres
| false, PostDouble (post, _, _ ) -> post
*)
in
let query =
match order with
| So -> raise (Crash (Printf.sprintf "so in knot %s" (string_of_knot knot)))
| Lo
| Go -> _recImplies sourcepost bassert
| Bo -> modalq sourcenode sourcepost
(fun f -> match f.fnode with Bfr (None,NoHook,f) -> Some f | _ -> None)
(_recBfr None NoHook)
bassert
| Uo -> modalq sourcenode sourcepost
(fun f -> match f.fnode with Univ (NoHook,f) -> Some f | _ -> None)
(_recUniv NoHook)
bassert
in
let stringfun () =
Printf.sprintf "inheritance of embroidery %s from source postcondition %s in constraint %s: %s->%s"
(string_of_formula bassert)
(string_of_formula sourcepost)
(string_of_order (order_of_stitch stitch))
(string_of_node bnode)
(string_of_node cnode)
in
check_taut (pos_of_stitch stitch) stringfun query
;
(* (* inheritance of location *)
(match locopt_of_stitch stitch with
| Some loc ->
(match sourcepost_of_stitch Elaboration stitch with
| PostSingle pre, _ ->
report (Error (stitch.stitchpos,
Printf.sprintf "stitch has reservation %s, but source %s \
doesn't have a reserved postcondition"
(string_of_location loc)
blab
)
)
| PostDouble (_, ploc, _), _
when not (Location.eq ploc loc) ->
report (Error (stitch.stitchpos,
Printf.sprintf "stitch has reservation %s, but source %s \
has postcondition reservation %s"
(string_of_location loc)
blab
(string_of_location ploc)
)
)
| _ -> () (* double, same loc *)
)
| None -> () (* not a reserved stitch *)
)
;
*)
(* external stability of stitch *)
List.iter (check_external_stability (pos_of_stitch stitch) (* (locopt_of_stitch stitch) *) bassert) rely;
(* here goes with internal stability *)
(* we have a constraint b->c. Find relevant so paths *)
let bcset = OPGraph.paths bnode cnode opgraph in
(* I _think_ it's right to filter bcset when it goes to a control expression *)
let bcset =
if is_control clab labmap then
let tnode = CEnode (clab,true) in
let fnode = CEnode (clab,false) in
let not_through_c (_,_,nodes) =
not (NodeSet.mem tnode nodes) && not (NodeSet.mem fnode nodes)
in
OPSet.filter not_through_c bcset
else bcset
in
let enclosed_filter outerps =
(function (So,path,_) -> List.for_all (encloses outerps <.> get_parents <.> label_of_node) path
| _ -> false
)
in
(* if a stitch pierces a loop, then the target->target so paths count too, including target ... *)
let ccset =
match inneropt with
| Some inner_paths -> inner_paths
| None ->
(let sourceps = get_parents blab in
let targetps = get_parents clab in
match weakest_inner_loop (common_ancestors sourceps targetps) targetps with
| None -> OPSet.empty (* can't happen, but never mind *)
| Some innerps ->
if !verbose || !Settings.verbose_knots then
Printf.printf "\n%s: stitch %s pierces loop %s"
(string_of_sourcepos (pos_of_stitch stitch))
(string_of_stitch stitch)
(Option.string_of_option string_of_parentid (pidopt innerps));
let extra_paths = OPGraph.paths cnode cnode opgraph in
OPSet.filter (enclosed_filter innerps) extra_paths
)
in
if !verbose || !Settings.verbose_knots then
Printf.printf "\nbcset = %s\nccset = %s" (OPSet.to_string bcset) (OPSet.to_string ccset);
let bcloopps = common_ancestors (get_parents blab) (get_parents clab) in
if !verbose || !Settings.verbose_knots then
Printf.printf "\nbcloop = %s"
(Option.string_of_option (bracketed_string_of_pair string_of_int string_of_scloc) (pidopt bcloopps));
(* we need only consider paths which stay within the loop enclosing b->c *)
let bcset = OPSet.filter (enclosed_filter bcloopps) bcset in
if !verbose || !Settings.verbose_knots then
Printf.printf "\nbcset filtered = %s" (OPSet.to_string bcset);
(* concatenate bcset and ccset paths *)
let bccset =
if OPSet.is_empty bcset then ccset else
if OPSet.is_empty ccset then bcset else
(let crossprod = OPSet.elements bcset >< OPSet.elements ccset in
let combine (_,p1,s1) (_,p2,s2) = So,p1@(cnode::p2),NodeSet.add cnode (NodeSet.union s1 s2) in
let r = OPSet.union bcset (OPSet.of_list (List.map (uncurry2 combine) crossprod)) in
if !verbose || !Settings.verbose_knots then
Printf.printf "\nbccset = %s" (OPSet.to_string r);
r
)
in
let interferes_before anode =
if anode=bnode then OPSet.empty else
(* deal with the possibility that a is a store-conditional *)
(let abset = OPGraph.paths anode bnode opgraph in
let alab = label_of_node anode in
let abset =
if is_control alab labmap then
(* store-conditional is dangerous on its 't' path *)
(let assignstep = CEnode (alab, true) in
OPSet.filter (fun (_,_,nset) -> NodeSet.mem assignstep nset) abset
)
else abset
in
if !verbose || !Settings.verbose_knots then
Printf.printf "\nabset %s->%s = %s" (string_of_node anode) (string_of_node bnode)
(OPSet.to_string abset);
so_butnot_constraint is_lo_opath abset
)
in
let interferes_after anode =
if cnode=anode then OPSet.empty else
(* take notice of the alpha/alpha(t)/alpha(f) stuff *)
(let caset =
if is_control clab labmap then
let direct b =
let paths = OPGraph.paths (CEnode (clab,b)) anode opgraph in
let other = CEnode (clab, not b) in
OPSet.filter (fun (_,_,nset) -> not (NodeSet.mem other nset)) paths
in
OPSet.union (direct true) (direct false)
else OPGraph.paths cnode anode opgraph
in
if !verbose || !Settings.verbose_knots then
Printf.printf "\ncaset %s->%s (%B) = %s" (string_of_node cnode) (string_of_node anode)
(is_control clab labmap) (OPSet.to_string caset);
so_butnot_constraint is_lo_opath caset
)
in
let cassign at =
let alab = at.tripletlab.lablab in
let anode = Cnode alab in
if !verbose || !Settings.verbose_knots then
Printf.printf "\n--checking assign %s" alab;
let vcheck lpk paths =
if !verbose || !Settings.verbose_knots && not (OPSet.is_empty paths) then
Printf.printf "\n%s %s"
(string_of_loparkind lpk)
(OPSet.to_string paths);
lpk, paths
in
let aintf = intf_of_ct Elaboration at in
let screg = !Settings.param_SCreg && Com.is_reg_assign at in
let interferes =
[vcheck InsideLo (OPSet.filter (fun (_,_,nodeset) -> NodeSet.mem anode nodeset)
bccset
);
(if screg then
InsideLo, OPSet.empty
else
vcheck BeforeLo (interferes_before anode)
);
(if screg then
AfterLo, OPSet.empty
else
vcheck AfterLo (interferes_after anode)
)
]
in
let check_lo aintf =
match Option.findfirst (not <.> OPSet.is_empty <.> sndof2) interferes with
| None -> ()
| Some (direction, opset) ->
(* we want the internal interference, unweakened for the guarantee *)
let reportpaths direction opset =
let singpre =
Printf.sprintf "there is %s '%s' so path"
(match direction with
| InsideLo
| AfterLo -> "an"
| BeforeLo -> "a"
)
(string_of_loparkind direction)
in
let plurpre =
Printf.sprintf "there are %s paths" (string_of_loparkind direction)
in
let pathlims =
match direction with
| InsideLo -> bnode, cnode
| BeforeLo -> anode, bnode
| AfterLo -> cnode, anode
in
Listutils.prefixed_phrase_of_list
(string_of_path <.> uncurry2 completepath_of_opath pathlims)
singpre
plurpre
(OPSet.elements opset)
in
let stringfun () =
Printf.sprintf "lo-parallel (internal) stability of %s against interference %s of command %s\
\n -- %s and no corresponding lo path"
(string_of_formula bassert)
(string_of_intfdesc aintf)
(string_of_label at.tripletlab.lablab)
(reportpaths direction opset)
in
if NameSet.is_empty (NameSet.inter (Formula.frees bassert)
(Intfdesc.assigned aintf)
)
then
avoided (pos_of_stitch stitch) "Z3 check" stringfun
else
(let scq =
Stability.sc_stable_query_intfdesc bassert aintf
in
check_taut (pos_of_stitch stitch) stringfun scq
)
in
(* match aintf with
| IntfSingle i -> check_lo i
| IntfDouble (i,ires) -> check_lo i; check_lo ires
*)
check_lo aintf
in
List.iter cassign assigns;
in
if !verbose || !Settings.verbose_knots then
Printf.printf "\n-- looking at knot %s inneropt %s"
(string_of_knot knot)
(Option.string_of_option OPSet.to_string inneropt);
match knot.knotnode with
| KnotAlt (k1,k2) -> let inner = KnotMap.find knot knotmap in
Knot.fold (cstitch (Some inner)) () k1;
check_knot clab rely assigns (Some inner) k2
| _ -> Knot.fold (cstitch inneropt) () knot
(* end of check_knot *)
in
let check_knot_of_triplet rely assigns string_of triplet =
if !verbose then
Printf.printf "\nlooking at triplet %s" (string_of_triplet string_of triplet);
check_knot triplet.tripletlab.lablab rely assigns None (triplet.tripletknot)
in
let cbup order_filter constraint_stab constraint_string needed vassigns triplet =
let check (at,bt) =
if at=bt then () else
if !Settings.param_SCloc &&
(let aves = Assign.loces (assign_of_triplet at) in
let bves = Assign.loces (assign_of_triplet bt) in
match aves, bves with
| (av,_)::_, (bv,_)::_ -> av=bv
| _ -> false
)
then ()
else
(let alab = at.tripletlab.lablab in
let blab = bt.tripletlab.lablab in
let abset = OPGraph.paths (Cnode alab) (Cnode blab) opgraph in
let opset = so_butnot_constraint order_filter abset in
if not (OPSet.is_empty opset) then
(let aintf = intf_of_ct Interference at in
let bintf = intf_of_ct Interference bt in
(* now that this has all doubled up, I could do with a Map here.
Wrong: check_taut is memoised, so we're ok.
*)
let check_buo aintf bintf =
let stringfun () =
Printf.sprintf "%s-parallel (in-flight) stability of %s against interference %s of command %s\
\n -- there %s"
constraint_string
(string_of_intfdesc aintf)
(string_of_intfdesc bintf)
(string_of_label blab)
(Listutils.prefixed_phrase_of_list
(string_of_path <.>
completepath_of_opath (Cnode alab) (Cnode blab)
)
"is a path"
"are paths"
(OPSet.elements opset)
)
in