Source file wpo.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
open LogicUsage
open VCS
open Cil_types
open Cil_datatype
open Lang
type index =
| Axiomatic of string option
| Function of kernel_function * string option
let bar = String.make 60 '-'
let flow = ref false
let pp_index fmt = function
| Axiomatic None -> Format.pp_print_string fmt "Axiomatics"
| Axiomatic (Some a) -> Format.pp_print_string fmt a
| Function(f,None) -> Kernel_function.pretty fmt f
| Function(f,Some b) -> Format.fprintf fmt "%a for %s:" Kernel_function.pretty f b
let pp_axiomatics fmt ax =
flow := true ;
match ax with
| None -> Format.fprintf fmt "%s@\n Global@\n%s@\n@\n" bar bar
| Some a -> Format.fprintf fmt "%s@\n Axiomatic '%s'@\n%s@\n@\n" bar a bar
let pp_function fmt kf bhv =
flow := true ;
match bhv with
| None ->
Format.fprintf fmt
"%s@\n Function %s@\n%s@\n@\n"
bar (Kernel_function.get_name kf) bar
| Some bhv ->
Format.fprintf fmt
"%s@\n Function %s with behavior %s@\n%s@\n@\n"
bar (Kernel_function.get_name kf) bhv bar
let pp_warnings fmt ws =
List.iter (fun w -> Format.fprintf fmt "%a@\n" Warning.pretty w) ws
module DISK =
struct
let file ~id ~model ?prover ?suffix ~ext () =
let mid = Wp_parameters.get_output_dir (WpContext.MODEL.id model) in
let buffer = Buffer.create 80 in
let fmt = Format.formatter_of_buffer buffer in
Format.fprintf fmt "%s/%s" (mid :> string) id ;
(match prover with None -> () | Some p ->
Format.fprintf fmt "_%s" (filename_for_prover p)) ;
(match suffix with None -> () | Some s ->
Format.fprintf fmt "_%s" s) ;
Format.fprintf fmt ".%s" ext ;
Format.pp_print_flush fmt ();
Filepath.Normalized.of_string (Buffer.contents buffer)
let file_logout ~pid ~model ~prover =
let id = WpPropId.get_propid pid in
file ~id ~model ~prover ~ext:"out" ()
let file_logerr ~pid ~model ~prover =
let id = WpPropId.get_propid pid in
file ~id ~model ~prover ~ext:"err" ()
let file_goal ~pid ~model ~prover =
let ext = match prover with
| Qed -> "qed"
| Why3 _ -> "why"
| Tactical -> "tac"
in
let id = WpPropId.get_propid pid in
file ~id ~model ~prover ~ext ()
end
module GOAL =
struct
type t = {
mutable time : float ;
mutable simplified : bool ;
mutable sequent : Conditions.sequent ;
mutable opened : F.pred ;
mutable closed : F.pred ;
mutable probes : F.term Probe.Map.t ;
}
let empty = Conditions.empty
let dummy = {
time = 0.0 ;
simplified = false ;
sequent = empty , F.p_false ;
opened = F.p_false ;
closed = F.p_false ;
probes = Probe.Map.empty ;
}
let trivial = {
time = 0.0 ;
simplified = true ;
sequent = empty , F.p_true ;
opened = F.p_true ;
closed = F.p_true ;
probes = Probe.Map.empty ;
}
let make sequent = {
time = 0.0 ;
simplified = false ;
sequent = sequent ;
opened = F.p_false ;
closed = F.p_false ;
probes = Probe.Map.empty ;
}
let is_computed g = g.simplified
let is_trivial g = Conditions.is_trivial g.sequent
let dkey = Wp_parameters.register_category "qed"
let apply option phi g =
try
Async.yield () ;
Wp_parameters.debug ~dkey "Apply %s" option ;
g.sequent <- phi g.sequent ;
with exn when Wp_parameters.protect exn ->
Wp_parameters.warning ~current:false ~once:true
"Goal simplification aborted (%s):@\n\
Exception %S@\n\
Re-run with debug level 1+ for details."
option (Printexc.to_string exn)
let default_simplifiers = [
Wp_parameters.SimplifyIsCint.get, Cint.is_cint_simplifier ;
Wp_parameters.SimplifyLandMask.get, Cint.mask_simplifier ;
]
let preprocess g =
if Wp_parameters.Let.get () then
begin
apply "introduction" Conditions.introduction_eq g ;
let fold acc (get,solver) = if get () then solver::acc else acc in
let solvers = List.fold_left fold [] default_simplifiers in
apply "-wp-simplify-*" (Conditions.simplify ~solvers) g ;
if Wp_parameters.FilterInit.get ()
then apply "-wp-filter-init" Conditions.init_filter g ;
if Wp_parameters.Prune.get ()
then apply "-wp-pruning" (Conditions.pruning ~solvers) g ;
if Wp_parameters.Filter.get ()
then apply "-wp-filter" Conditions.filter g ;
if Wp_parameters.Parasite.get ()
then apply "-wp-parasite" Conditions.parasite g ;
end
else
begin
if Wp_parameters.Clean.get ()
then apply "-wp-clean" Conditions.clean g ;
end ;
begin
if Conditions.is_trivial g.sequent then
g.sequent <- Conditions.trivial ;
g.opened <- Conditions.property g.sequent ;
g.closed <- F.p_close g.opened ;
end
let safecompute ~pid g =
begin
g.simplified <- true ;
let timer = ref 0.0 in
Wp_parameters.debug ~dkey "Simplify %a" WpPropId.pretty pid ;
Command.time ~rmax:timer preprocess g ;
Wp_parameters.debug ~dkey "Simplification time: %a"
Rformat.pp_time !timer ;
g.time <- !timer ;
g.probes <- Conditions.probes @@ fst g.sequent ;
end
let compute ~pid g =
if not g.simplified then
Lang.local ~vars:(Conditions.vars_seq g.sequent)
(safecompute ~pid) g
let compute_proof ~pid ?(opened=false) g =
compute ~pid g ; if opened then g.opened else g.closed
let compute_probes ~pid g = compute ~pid g ; g.probes
let compute_descr ~pid g = compute ~pid g ; g.sequent
let get_descr g = g.sequent
let qed_time g = g.time
end
module VC_Annot =
struct
type t = {
axioms : Definitions.axioms option ;
goal : GOAL.t ;
tags : Splitter.tag list ;
warn : Warning.t list ;
deps : Property.Set.t ;
path : Stmt.Set.t ;
source : (stmt * Mcfg.goal_source) option ;
}
let repr = {
axioms = None ;
goal = GOAL.dummy ;
tags = [] ;
warn = [] ;
deps = Property.Set.empty ;
path = Stmt.Set.empty ;
source = None ;
}
let resolve ~pid vcq = GOAL.compute_proof ~pid vcq.goal == Lang.F.p_true
let is_trivial vcq = GOAL.is_trivial vcq.goal
let pp_effect fmt s e =
let loc = fst (Stmt.loc s) in
let line = loc.Filepath.pos_lnum in
let desc = match e with
| Mcfg.FromCode -> "Effect"
| Mcfg.FromCall -> "Call Effect"
| Mcfg.FromReturn -> "Call Result"
in
Format.fprintf fmt "%s at line %d@\n" desc line
let pp_terminates fmt s e =
let loc = fst (Stmt.loc s) in
let line = loc.Filepath.pos_lnum in
let desc = match e with
| Mcfg.Loop -> "Loop termination"
| Mcfg.Terminates -> "Call terminates"
| Mcfg.Decreases -> "Call decreases"
| Mcfg.MissingTerminates -> "Call terminates (missing terminates)"
| Mcfg.MissingDecreases -> "Call terminates (missing decreases)"
| Mcfg.Dependencies -> "Call terminates (dependencies)"
in
Format.fprintf fmt "%s at line %d@\n" desc line
let pp_source fmt = function
| None -> ()
| Some (s, Mcfg.Effect e) -> pp_effect fmt s e
| Some (s, Mcfg.Terminates e) -> pp_terminates fmt s e
let pretty fmt pid vc results =
begin
Format.fprintf fmt "@{<bf>Goal@} %a:@\n" WpPropId.pretty pid ;
pp_source fmt vc.source ;
if vc.tags <> [] then
begin
Format.fprintf fmt "@[<hov 2>@{<bf>Tags@}:" ;
List.iter (fun tg -> Format.fprintf fmt "@ %a" Splitter.pretty tg) vc.tags ;
Format.fprintf fmt "@].@\n" ;
end ;
begin match vc.axioms with
| Some (_, depends) when depends <> [] ->
Format.fprintf fmt "@[<hov 2>@{<bf>Assume Lemmas@}:" ;
List.iter
(fun a -> Format.fprintf fmt "@ '%s'" a.lem_name)
depends ;
Format.fprintf fmt "@]@." ;
| _ -> ()
end ;
pp_warnings fmt vc.warn ;
Pcond.pretty fmt (GOAL.compute_descr ~pid vc.goal) ;
List.iter
(fun (prover,result) ->
if result.verdict <> NoResult then
Format.fprintf fmt "Prover %a returns %t@\n"
pp_prover prover
(pp_result_qualif prover result) ;
if Wp_parameters.CounterExamples.get () then
pp_model fmt result.prover_model
) results ;
end
end
type po = t and t = {
po_gid : string ;
po_sid : string ;
po_name : string ;
po_idx : index ;
po_model : WpContext.model ;
po_pid : WpPropId.prop_id ;
po_formula : VC_Annot.t ;
}
let get_index w = w.po_idx
let get_label w = WpPropId.label_of_prop_id w.po_pid
let get_model x = x.po_model
let get_scope w = match w.po_idx with
| Axiomatic _ -> WpContext.Global
| Function(kf,_) -> WpContext.Kf kf
let get_context w = w.po_model , get_scope w
let get_depend wpo =
let open LogicUsage in
let deps = wpo.po_formula.deps in
let axioms = wpo.po_formula.axioms in
List.rev_append
(Option.fold ~none:[] ~some:(fun (_, l) -> List.map ip_lemma l) axioms)
(Property.Set.elements deps)
let get_file_logout w prover =
DISK.file_logout ~pid:w.po_pid ~model:(get_model w) ~prover
let get_file_logerr w prover =
DISK.file_logerr ~pid:w.po_pid ~model:(get_model w) ~prover
module Index =
struct
type t = index
let cmpopt a b =
match a,b with
| Some a,Some b -> String.compare a b
| None,Some _ -> (-1)
| Some _,None -> 1
| None,None -> 0
let compare a b =
match a,b with
| Axiomatic a , Axiomatic b -> cmpopt a b
| Axiomatic _ , Function _ -> (-1)
| Function _ , Axiomatic _ -> 1
| Function(f,a) , Function(g,b) ->
let c =
if Kernel_function.equal f g then 0 else
String.compare
(Kernel_function.get_name f)
(Kernel_function.get_name g)
in
if c=0 then cmpopt a b else c
end
module S =
Datatype.Make_with_collections
(struct
type t = po
include Datatype.Undefined
let hash a = FCHashtbl.hash a.po_gid
let equal a b = (a.po_gid = b.po_gid)
let compare a b =
let c = Index.compare a.po_idx b.po_idx in
if c<>0 then c else
let c = WpPropId.compare_prop_id a.po_pid b.po_pid in
if c<>0 then c else
let ma = get_model a |> WpContext.MODEL.descr in
let mb = get_model b |> WpContext.MODEL.descr in
let c = String.compare ma mb in
if c<>0 then c else
String.compare a.po_gid b.po_gid
let pretty fmt wpo = Format.pp_print_string fmt wpo.po_name
let name = "Wpo.po"
let reprs =
[{
po_idx = Function(List.hd Kernel_function.reprs,Some "default") ;
po_pid = List.hd WpPropId.PropId.reprs;
po_sid = "";
po_gid = "";
po_model = WpContext.MODEL.repr ;
po_name = "dummy";
po_formula = VC_Annot.repr ;
}]
end)
let () = Type.set_ml_name S.ty (Some "Wpo.po")
module WpoType = S
module ProverType =
Datatype.Make
(struct
type t = prover
include Datatype.Undefined
let name = "Wpo.prover"
let reprs = [ Qed ]
end)
let () = Type.set_ml_name ProverType.ty (Some "Wpo.prover")
module ResultType =
Datatype.Make
(struct
type t = result
include Datatype.Undefined
let name = "Wpo.result"
let reprs =
List.map VCS.result
[ Valid ; Unknown ; Timeout ; Failed ]
end)
let () = Type.set_ml_name ResultType.ty (Some "Wpo.result")
let get_gid g = g.po_gid
let get_property g = WpPropId.property_of_id g.po_pid
let qed_time wpo =
GOAL.qed_time wpo.po_formula.goal
let is_tactic t = WpPropId.is_tactic t.po_pid
let is_smoke_test t = WpPropId.is_smoke_test t.po_pid
module Hproof = Hashtbl.Make(Datatype.Pair(Datatype.String)(Property))
module Results =
struct
type t = {
mutable dps : result Pmap.t ;
}
let create () = { dps = Pmap.empty }
let get w p =
Pmap.find p w.dps
let clear w =
Pmap.iter (fun _ r ->
match r.verdict with
| VCS.Computing kill -> kill ()
| _ -> ()
) w.dps ;
w.dps <- Pmap.empty
let replace w p r =
begin
if p = Qed then
(w.dps <- Pmap.filter (fun _ r -> VCS.is_verdict r) w.dps) ;
w.dps <- Pmap.add p r w.dps
end
let list w =
List.filter (fun (_,r) -> not @@ VCS.is_none r) @@ Pmap.bindings w.dps
end
let modified_hooks : (t -> unit) list ref = ref []
let removed_hooks : (t -> unit) list ref = ref []
let cleared_hooks : (unit -> unit) list ref = ref []
let add_modified_hook f = modified_hooks := !modified_hooks @ [f]
let add_removed_hook f = removed_hooks := !removed_hooks @ [f]
let add_cleared_hook f = cleared_hooks := !cleared_hooks @ [f]
let modified g =
List.iter (fun f -> f g) !modified_hooks
let removed g =
List.iter (fun f -> f g) !removed_hooks
module WPOset = WpoType.Set
module WPOmap = WpoType.Map
module Gmap = Map.Make(Index)
module Fmap = Kernel_function.Map
module Pmap = Property.Map
let index_wpo iadd iget k w m =
let set = try iget k m with Not_found -> WPOset.empty in
iadd k (WPOset.add w set) m
let unindex_wpo iadd iget k w m =
try
let set = iget k m in
iadd k (WPOset.remove w set) m
with Not_found -> m
type system = {
mutable wpo_idx : WPOset.t Gmap.t ;
mutable wpo_kf : WPOset.t Fmap.t ;
mutable wpo_ip : WPOset.t Pmap.t ;
mutable age : int WPOmap.t ;
mutable results : Results.t WPOmap.t ;
proofs : WpPropId.proof Hproof.t ;
}
let create_system () =
{
wpo_idx = Gmap.empty ;
wpo_kf = Fmap.empty ;
wpo_ip = Pmap.empty ;
results = WPOmap.empty ;
age = WPOmap.empty ;
proofs = Hproof.create 131 ;
}
let clear_system system =
begin
system.wpo_idx <- Gmap.empty ;
system.wpo_kf <- Fmap.empty ;
system.wpo_ip <- Pmap.empty ;
system.results <- WPOmap.empty ;
system.age <- WPOmap.empty ;
Hproof.clear system.proofs ;
List.iter (fun f -> f ()) !cleared_hooks ;
end
module SYSTEM = State_builder.Ref
(Datatype.Make
(struct
include Datatype.Undefined
type t = system
let name = "Wpo.SYSTEM.Datatype"
let reprs = [ create_system () ]
let mem_project = Datatype.never_any_project
end))
(struct
let name = "Wpo.SYSTEM.System"
let dependencies = [ Ast.self ]
let default = create_system
end)
let clear () = clear_system (SYSTEM.get ())
let added = ref 0
let age g =
let system = SYSTEM.get () in
try WPOmap.find g system.age with Not_found -> 0
let current_age = ref (-1)
let proof g ip = ( get_context g |> WpContext.S.id , ip )
let add g =
let system = SYSTEM.get () in
begin
let ip = WpPropId.property_of_id g.po_pid in
Hproof.remove system.proofs (proof g ip) ;
let age = incr current_age; !current_age in
system.age <- WPOmap.add g age system.age ;
system.results <- WPOmap.remove g system.results ;
system.wpo_idx <- index_wpo Gmap.add Gmap.find g.po_idx g system.wpo_idx ;
system.wpo_ip <- index_wpo Pmap.add Pmap.find ip g system.wpo_ip ;
begin
match g.po_idx with
| Function(kf,_) ->
system.wpo_kf <- index_wpo Fmap.add Fmap.find kf g system.wpo_kf
| _ -> ()
end ;
incr added ;
if !added >= 100 then
begin
added := 0 ;
Gmap.iter
(fun _ ws -> WPOset.iter (fun _ -> incr added) ws)
system.wpo_idx ;
if not (Wp_parameters.has_dkey VCS.dkey_shell) then
Wp_parameters.feedback ~ontty:`Feedback "Computing [%d goals...]" !added ;
added := 0 ;
end ;
modified g ;
end
let remove g =
let system = SYSTEM.get () in
begin
let ip = WpPropId.property_of_id g.po_pid in
system.wpo_idx <- unindex_wpo Gmap.add Gmap.find g.po_idx g system.wpo_idx ;
system.wpo_ip <- unindex_wpo Pmap.add Pmap.find ip g system.wpo_ip ;
begin
match g.po_idx with
| Function(kf,_) ->
system.wpo_kf <- unindex_wpo Fmap.add Fmap.find kf g system.wpo_kf
| Axiomatic _ -> ()
end ;
system.results <- WPOmap.remove g system.results ;
Hproof.remove system.proofs (proof g ip) ;
removed g ;
end
let warnings wpo = wpo.po_formula.VC_Annot.warn
let get_target g = WpPropId.property_of_id g.po_pid
let get_proof g =
let system = SYSTEM.get () in
let target = get_target g in
let status =
try
let proof = Hproof.find system.proofs (proof g target) in
if is_smoke_test g then
if WpPropId.is_proved proof then `Failed else
if WpPropId.is_invalid proof then `Passed else
`Unknown
else
if WpPropId.is_proved proof then `Passed else `Unknown
with Not_found -> `Unknown
in status , target
let find_proof system g =
let pi = proof g (WpPropId.property_of_id g.po_pid) in
try Hproof.find system.proofs pi
with Not_found ->
let proof = WpPropId.create_proof g.po_pid in
Hproof.add system.proofs pi proof ; proof
let clear_results g =
let system = SYSTEM.get () in
try
let rs = WPOmap.find g system.results in
Results.clear rs ;
modified g ;
with Not_found -> ()
let set_result g p r =
let system = SYSTEM.get () in
let rs =
try WPOmap.find g system.results
with Not_found ->
let rs = Results.create () in
system.results <- WPOmap.add g rs system.results ; rs
in
Results.replace rs p r ;
if not (WpPropId.is_check g.po_pid) &&
not (WpPropId.is_tactic g.po_pid) &&
VCS.is_verdict r
then
begin
let smoke = is_smoke_test g in
let proof = find_proof system g in
let emitter = WpContext.get_emitter g.po_model in
let target = WpPropId.target proof in
let unproved = not (WpPropId.is_proved proof) in
begin
if VCS.is_valid r then
WpPropId.add_proof proof g.po_pid (get_depend g)
else if smoke then
WpPropId.add_invalid_proof proof ;
end ;
let proved = WpPropId.is_proved proof in
let status =
if smoke then
if proved
then Property_status.False_if_reachable
else if WpPropId.is_invalid proof
then Property_status.True
else Property_status.Dont_know
else
if proved
then Property_status.True
else Property_status.Dont_know
in
let hyps = if smoke then [] else WpPropId.dependencies proof in
Property_status.emit emitter ~hyps target status ;
if smoke && unproved && proved then
WpReached.set_doomed emitter g.po_pid ;
end ;
modified g
let has_verdict g p =
let system = SYSTEM.get () in
try VCS.is_verdict (Results.get (WPOmap.find g system.results) p)
with Not_found -> false
let get_result g p : VCS.result =
let system = SYSTEM.get () in
try Results.get (WPOmap.find g system.results) p
with Not_found -> VCS.no_result
let get_results g =
let system = SYSTEM.get () in
try Results.list @@ WPOmap.find g system.results
with Not_found -> []
let get_prover_results g =
List.filter (fun (p,_) -> VCS.is_prover p) @@ get_results g
let is_trivial g =
VC_Annot.is_trivial g.po_formula
let reduce g =
let pid = g.po_pid in
WpContext.on_context (get_context g) (VC_Annot.resolve ~pid) g.po_formula
let resolve g =
let valid = reduce g in
if valid then
let result = VCS.result ~solver:(qed_time g) VCS.Valid in
( set_result g VCS.Qed result ; true )
else false
let computed g =
GOAL.is_computed g.po_formula.goal
let compute g =
let ctxt = get_context g in
let pid = g.po_pid in
g.po_formula.axioms ,
let goal = g.po_formula.goal in
let qed = GOAL.is_computed goal in
let seq = WpContext.on_context ctxt (GOAL.compute_descr ~pid) goal in
if not qed then modified g ; seq
let is_fully_valid g =
is_trivial g ||
List.exists (fun (_,r) -> VCS.is_valid r) @@ get_results g
let is_locally_valid g =
is_trivial g ||
List.exists (fun (p,r) -> VCS.is_prover p && VCS.is_valid r) @@ get_results g
let all_not_valid g =
not (is_trivial g) &&
List.for_all (fun (_,r) -> VCS.is_not_valid r) @@ get_results g
let is_passed g =
if is_smoke_test g then
all_not_valid g
else
is_fully_valid g
let has_unknown g =
not (is_fully_valid g) &&
List.exists
(fun (p,r) -> VCS.is_prover p && VCS.is_verdict r && not (VCS.is_valid r))
(get_results g)
let pp_title fmt w = Format.pp_print_string fmt w.po_name
let pp_goal_model fmt w =
VC_Annot.pretty fmt w.po_pid w.po_formula (get_results w)
let pp_goal fmt w = WpContext.on_context (get_context w) (pp_goal_model fmt) w
let pp_flow fmt =
Format.fprintf fmt "@\n%s@\n" bar ;
flow := false
let pp_goal_flow fmt g =
begin
if not !flow then Format.pp_print_newline fmt () ;
pp_goal fmt g ;
Format.fprintf fmt "@\n%s@." bar ;
flow := false ;
end
type part =
| Pnone
| Paxiomatic of string option
| Pbehavior of kernel_function * string option
let iter ?ip ?index ?on_axiomatics ?on_behavior ?on_goal () =
let system = SYSTEM.get () in
let current = ref Pnone in
let apply_lemma a =
match on_axiomatics with None -> () | Some phi -> phi a in
let apply_behavior f bhv =
match on_behavior with None -> () | Some phi -> phi f bhv in
let on_part idx =
match !current , idx with
| Paxiomatic a , Axiomatic b when a=b -> ()
| _ , Axiomatic b -> apply_lemma b ; current := Paxiomatic b
| Pbehavior(f,None) , Function(g,None) when Kernel_function.equal f g -> ()
| Pbehavior(f,Some a) , Function(g,Some b) when Kernel_function.equal f g && a=b -> ()
| _ , Function(g,bhv) -> apply_behavior g bhv ; current := Pbehavior(g,bhv)
in
let on_goals poset =
if not (WPOset.is_empty poset) then
begin
match on_goal with
| None -> ()
| Some phi -> WPOset.iter phi poset
end
in
match index,ip with
| None,None ->
Gmap.iter (fun idx ws -> on_part idx ; on_goals ws) system.wpo_idx
| _,Some ip ->
begin
match on_goal with
| None -> ()
| Some phi ->
let poset =
try Pmap.find ip system.wpo_ip
with Not_found -> WPOset.empty in
WPOset.iter phi poset
end
| Some (Function(kf,None)),None ->
begin
try on_goals (Fmap.find kf system.wpo_kf)
with Not_found -> ()
end
| Some idx,None ->
begin
try on_goals (Gmap.find idx system.wpo_idx)
with Not_found -> ()
end
let iter_on_goals f = iter ~on_goal:f ()
let goals_of_property prop =
let system = SYSTEM.get () in
let poset =
try Pmap.find prop system.wpo_ip
with Not_found -> WPOset.empty
in
WPOset.elements poset
class type generator =
object
method model : WpContext.model
method compute_ip : Property.t -> t Bag.t
method compute_call : stmt -> t Bag.t
method compute_main :
?fct:Wp_parameters.functions ->
?bhv:string list ->
?prop:string list ->
unit -> t Bag.t
end