Source file wpApi.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
module P = Server.Package
module D = Server.Data
module R = Server.Request
module S = Server.States
module Md = Markdown
module AST = Server.Kernel_ast
module WP_Prover = Prover
let package = P.package ~plugin:"wp" ~title:"WP Main Services" ()
module INDEX = State_builder.Ref
(Datatype.Make
(struct
include Datatype.Undefined
type t = (string,Wpo.t) Hashtbl.t
let name = "WpApi.INDEX.Datatype"
let reprs = [ Hashtbl.create 0 ]
let mem_project = Datatype.never_any_project
end))
(struct
let name = "WpApi.INDEX"
let dependencies = [ Ast.self ]
let default () = Hashtbl.create 0
end)
let indexGoal g =
let id = g.Wpo.po_gid in
let index = INDEX.get () in
if not (Hashtbl.mem index id) then Hashtbl.add index id g ; id
module Goal : D.S with type t = Wpo.t =
struct
type t = Wpo.t
let jtype = D.declare ~package ~name:"goal"
~descr:(Md.plain "Proof Obligations") (Jkey "wpo")
let of_json js = Hashtbl.find (INDEX.get ()) (Json.string js)
let to_json g = `String (indexGoal g)
end
module Prover =
struct
type t = Prover.t
let jtype = D.declare ~package ~name:"prover"
~descr:(Md.plain "Prover Identifier") (Jkey "prover")
let to_json prv = `String (WP_Prover.ident prv)
let of_json js =
match Prover.parse @@ Json.string js with
| Some prv -> prv
| None -> D.failure "Unknown prover name"
end
module Provers = D.Jlist(Prover)
let signal = ref None
let getProvers () =
List.filter WP_Prover.is_extern @@ WP_Prover.provers ()
let () =
R.register ~package
~name:"setProverState"
~descr:(Md.plain "Select/unselect prover")
~kind:`SET
~input:(module D.Jpair(Prover)(D.Jbool))
~output:(module D.Junit)
begin fun (p, v) ->
WP_Prover.set_prover p ~state:v ;
Option.iter R.emit !signal
end
let _ =
let s =
S.register_value
~package ~name:"provers"
~descr:(Md.plain "Get all available provers")
~output:(module Provers)
~get:(fun () -> getProvers())
()
in
signal := Some s
let _ : WP_Prover.t S.array =
let model = S.model () in
S.column ~name:"name" ~descr:(Md.plain "Prover Name")
~data:(module D.Jalpha) ~get:WP_Prover.name model ;
S.column ~name:"version" ~descr:(Md.plain "Prover Version")
~data:(module D.Jalpha) ~get:WP_Prover.version model ;
S.column ~name:"descr" ~descr:(Md.plain "Prover Full Name (description)")
~data:(module D.Jalpha) ~get:(WP_Prover.title ~version:true) model ;
S.column model ~name:"extern" ~descr:(Md.plain "Why3 or internal")
~data:(module D.Jbool) ~get:WP_Prover.is_extern ;
S.column model ~name:"auto" ~descr:(Md.plain "Automatic solver")
~data:(module D.Jbool) ~get:WP_Prover.is_auto ;
S.column model ~name:"active" ~descr:(Md.plain "Whether it is enabled")
~data:(module D.Jbool) ~get:WP_Prover.enabled ;
S.register_array ~package
~name:"ProverInfos" ~descr:(Md.plain "Available Provers")
~key:WP_Prover.ident
~keyName:"prover"
~keyType:Prover.jtype
~iter:(fun f -> List.iter f @@ WP_Prover.provers ())
~add_update_hook:WP_Prover.add_prover_update_hook
~add_reload_hook:WP_Prover.add_reload_hook
model
let _ =
S.register_state ~package
~name:"process"
~descr:(Md.plain "Server Processes")
~data:(module D.Jint)
~get:Wp_parameters.Procs.get
~set:(fun procs ->
Wp_parameters.Procs.set procs ;
ignore @@ ProverTask.server ~procs ())
~add_hook:Wp_parameters.Procs.add_hook_on_update ()
let _ =
S.register_state ~package
~name:"timeout"
~descr:(Md.plain "Prover's Timeout")
~data:(module D.Jint)
~get:Wp_parameters.Timeout.get
~set:Wp_parameters.Timeout.set
~add_hook:Wp_parameters.Timeout.add_hook_on_update ()
module CacheMode =
struct
include D.Enum
let dictionary : Cache.mode dictionary = dictionary ()
let tag name value = tag ~name ~descr:(Md.plain name) ~value dictionary
let none = tag "None" NoCache
let update = tag "Update" Update
let replay = tag "Replay" Replay
let rebuild = tag "Rebuild" Rebuild
let offline = tag "Offline" Offline
let cleanup = tag "Cleanup" Cleanup
let lookup = function
| Cache.NoCache -> none
| Update -> update
| Replay -> replay
| Rebuild -> rebuild
| Offline -> offline
| Cleanup-> cleanup
let () =
set_lookup dictionary lookup
include
(val publish
~package
~descr:(Md.plain "Cache mode")
~name:"CacheMode"
dictionary)
end
let _ =
S.register_state ~package
~name:"cacheMode"
~descr:(Md.plain "Current Cache mode")
~data:(module CacheMode)
~get:Cache.get_mode
~set:Cache.set_mode
~add_hook:Cache.add_hook_on_mode_update
()
let _ =
R.register
~package ~kind:`GET ~name:"isInteractiveProver"
~descr:(Md.plain "Tells whether the prover is interactive")
~input:(module Prover)
~output:(module D.Jbool)
(fun p -> not @@ WP_Prover.is_auto p)
module InteractiveMode =
struct
include D.Enum
let dictionary : WP_Prover.InteractiveMode.t dictionary = dictionary ()
let tag name value = tag ~name ~descr:(Md.plain name) ~value dictionary
let batch = tag "Batch" WP_Prover.InteractiveMode.Batch
let update = tag "Update" WP_Prover.InteractiveMode.Update
let edit = tag "Edit" WP_Prover.InteractiveMode.Edit
let fix = tag "Fix" WP_Prover.InteractiveMode.Fix
let fixup = tag "FixUpdate" WP_Prover.InteractiveMode.FixUpdate
let lookup = function
| WP_Prover.InteractiveMode.Batch -> batch
| Update -> update
| Edit -> edit
| Fix -> fix
| FixUpdate -> fixup
let () =
set_lookup dictionary lookup
include
(val publish
~package
~descr:(Md.plain "interactive mode")
~name:"InteractiveMode"
dictionary)
end
let _ =
S.register_state ~package
~name:"interactiveMode"
~descr:(Md.plain "Current interactive mode")
~data:(module InteractiveMode)
~get:WP_Prover.InteractiveMode.get
~set:WP_Prover.InteractiveMode.set
~add_hook:WP_Prover.InteractiveMode.add_hook_on_update
()
module TipMode =
struct
include D.Enum
let dictionary : WP_Prover.TipMode.t dictionary = dictionary ()
let tag name value = tag ~name ~descr:(Md.plain name) ~value dictionary
let batch = tag "Batch" WP_Prover.TipMode.Batch
let update = tag "Update" WP_Prover.TipMode.Update
let dry = tag "Dry" WP_Prover.TipMode.Dry
let init = tag "Init" WP_Prover.TipMode.Init
let lookup = function
| WP_Prover.TipMode.Batch -> batch
| Update -> update
| Dry -> dry
| Init -> init
let () =
set_lookup dictionary lookup
include
(val publish
~package
~descr:(Md.plain "TIP mode")
~name:"TipMode"
dictionary)
end
let _ =
S.register_state ~package
~name:"tipMode"
~descr:(Md.plain "Current Strategy Mode")
~data:(module TipMode)
~get:WP_Prover.TipMode.get
~set:WP_Prover.TipMode.set
~add_hook:WP_Prover.TipMode.add_hook_on_update
()
let _ =
S.register_state ~package
~name:"scripts"
~descr:(Md.plain "Whether scripts are enabled")
~data:(module D.Jbool)
~get:WP_Prover.use_scripts
~set:WP_Prover.set_use_scripts
~add_hook:WP_Prover.add_scripts_update_hook
()
let _ =
S.register_state ~package
~name:"strategies"
~descr:(Md.plain "Whether strategies are enabled")
~data:(module D.Jbool)
~get:WP_Prover.use_strategies
~set:WP_Prover.set_use_strategies
~add_hook:WP_Prover.add_scripts_update_hook
()
let _ =
S.register_state ~package
~name:"counterExamples"
~descr:(Md.plain "Enabled Counter Examples")
~data:(module D.Jbool)
~get:Wp_parameters.CounterExamples.get
~set:Wp_parameters.CounterExamples.set
~add_hook:Wp_parameters.CounterExamples.add_hook_on_update ()
module Result =
struct
type t = VCS.result
let jtype = D.declare ~package ~name:"result"
~descr:(Md.plain "Prover Result")
(Jrecord [
"descr", Jstring ;
"cached", Jboolean ;
"verdict", Jstring ;
"solverTime", Jnumber ;
"proverTime", Jnumber ;
"proverSteps", Jnumber ;
])
let of_json _ = failwith "Not implemented"
let to_json (r : VCS.result) = `Assoc [
"descr", `String (Pretty_utils.to_string VCS.pp_result r) ;
"cached", `Bool r.cached ;
"verdict", `String (VCS.name_of_verdict ~computing:true r.verdict) ;
"solverTime", `Float r.solver_time ;
"proverTime", `Float r.prover_time ;
"proverSteps", `Int r.prover_steps ;
]
end
module STATUS =
struct
type t = { smoke : bool ; verdict : VCS.verdict }
let jtype = D.declare ~package ~name:"status"
~descr:(Md.plain "Test Status")
(Junion [
Jkey "NORESULT" ;
Jkey "COMPUTING" ;
Jkey "FAILED" ;
Jkey "STEPOUT" ;
Jkey "UNKNOWN" ;
Jkey "VALID" ;
Jkey "PASSED" ;
Jkey "DOOMED" ;
])
let to_json { smoke ; verdict } =
`String begin
match verdict with
| Valid -> if smoke then "DOOMED" else "VALID"
| Invalid -> if smoke then "PASSED" else "INVALID"
| Unknown -> if smoke then "PASSED" else "UNKNOWN"
| Timeout -> if smoke then "PASSED" else "TIMEOUT"
| Stepout -> if smoke then "PASSED" else "STEPOUT"
| Failed -> "FAILED"
| NoResult -> "NORESULT"
| Computing _ -> "COMPUTING"
end
end
module STATS =
struct
type t = Stats.stats
let jtype = D.declare ~package ~name:"stats"
~descr:(Md.plain "Prover Result")
(Jrecord [
"summary", Jstring;
"tactics", Jnumber;
"proved", Jnumber;
"total", Jnumber;
])
let to_json cs : Json.t =
let cache = Cache.get_mode () in
let summary = Pretty_utils.to_string
(Stats.pp_stats ~shell:false ~cache) cs
in `Assoc [
"summary", `String summary ;
"tactics", `Int cs.tactics ;
"proved", `Int cs.proved ;
"total", `Int (Stats.subgoals cs) ;
]
end
let gmodel : Wpo.t S.model = S.model ()
let get_property g = Printer_tag.PIP (WpPropId.property_of_id g.Wpo.po_pid)
let get_marker g =
match g.Wpo.po_formula.source with
| Some(stmt,_) -> Printer_tag.localizable_of_stmt stmt
| None ->
let ip = WpPropId.property_of_id g.Wpo.po_pid in
match ip with
| IPOther { io_loc = OLStmt(_,stmt) } ->
Printer_tag.localizable_of_stmt stmt
| _ -> Printer_tag.PIP ip
let get_decl g = match g.Wpo.po_idx with
| Function(kf,_) -> Some (Printer_tag.SFunction kf)
| Axiomatic _ -> None
let get_fct g = match g.Wpo.po_idx with
| Function(kf,_) -> Some (Kernel_function.get_name kf)
| Axiomatic _ -> None
let get_bhv g = match g.Wpo.po_idx with
| Function(_,bhv) -> bhv
| Axiomatic _ -> None
let get_thy g = match g.Wpo.po_idx with
| Function _ -> None
| Axiomatic ax -> ax
let get_status g =
STATUS.{
smoke = Wpo.is_smoke_test g ;
verdict = (ProofEngine.consolidated g).best ;
}
let get_ast_dependencies g =
let open Wpo in
let module Stmts = Cil_datatype.Stmt.Set in
let module Props = Property.Set in
let add_stmt s l = Printer_tag.localizable_of_stmt s :: l in
let add_prop p l = Printer_tag.PIP p :: l in
Stmts.fold add_stmt g.po_formula.path @@
Props.fold add_prop g.po_formula.deps []
let () = S.column gmodel ~name:"marker"
~descr:(Md.plain "Associated Marker")
~data:(module AST.Marker) ~get:get_marker
let () = S.column gmodel ~name:"scope"
~descr:(Md.plain "Associated declaration, if any")
~data:(module D.Joption(AST.Decl)) ~get:get_decl
let () = S.column gmodel ~name:"property"
~descr:(Md.plain "Property Marker")
~data:(module AST.Marker) ~get:get_property
let () = S.option gmodel ~name:"fct"
~descr:(Md.plain "Associated function name, if any")
~data:(module D.Jstring) ~get:get_fct
let () = S.option gmodel ~name:"bhv"
~descr:(Md.plain "Associated behavior name, if any")
~data:(module D.Jstring) ~get:get_bhv
let () = S.option gmodel ~name:"thy"
~descr:(Md.plain "Associated axiomatic name, if any")
~data:(module D.Jstring) ~get:get_thy
let () = S.column gmodel ~name:"name"
~descr:(Md.plain "Informal Property Name")
~data:(module D.Jstring)
~get:(fun g -> g.Wpo.po_name)
let () = S.column gmodel ~name:"smoke"
~descr:(Md.plain "Smoking (or not) goal")
~data:(module D.Jbool) ~get:Wpo.is_smoke_test
let () = S.column gmodel ~name:"passed"
~descr:(Md.plain "Valid or Passed goal")
~data:(module D.Jbool) ~get:Wpo.is_passed
let () = S.column gmodel ~name:"status"
~descr:(Md.plain "Verdict, Status")
~data:(module STATUS) ~get:get_status
let () = S.column gmodel ~name:"stats"
~descr:(Md.plain "Prover Stats Summary")
~data:(module STATS) ~get:ProofEngine.consolidated
let () = S.column gmodel ~name:"proof"
~descr:(Md.plain "Proof Tree")
~data:(module D.Jbool)
~get:ProofEngine.has_proof
let () = S.option gmodel ~name:"script"
~descr:(Md.plain "Script File")
~data:(module D.Jstring)
~get:(fun wpo ->
match ProofSession.get wpo with
| NoScript -> None
| Script a | Deprecated a -> Some (Filepath.to_string_abs a))
let () = S.column gmodel ~name:"saved"
~descr:(Md.plain "Saved Script")
~data:(module D.Jbool)
~get:(fun wpo -> ProofEngine.get wpo = `Saved)
let () = S.column gmodel ~name:"deps"
~descr:(Md.plain "Dependencies")
~data:(module D.Jlist(AST.Marker))
~get:get_ast_dependencies
let filter hook fn = hook (fun g -> if not @@ Wpo.is_tactic g then fn g)
let (++) h1 h2 fn = h1 fn ; h2 fn
let goals =
let add_remove_hook =
filter Wpo.add_removed_hook in
let add_update_hook =
filter Wpo.add_modified_hook ++ ProofEngine.add_goal_hook in
let add_reload_hook = Wpo.add_cleared_hook in
S.register_array ~package ~name:"goals"
~descr:(Md.plain "Generated Goals")
~key:indexGoal
~keyName:"wpo"
~keyType:Goal.jtype
~iter:(filter Wpo.iter_on_goals)
~preload:ProofEngine.consolidate
~add_remove_hook
~add_update_hook
~add_reload_hook
gmodel
let () =
R.register ~package ~kind:`GET ~name:"getGoalsFromASTMarker"
~descr:(Md.plain "Get goals from AST marker")
~input:(module AST.Marker)
~output:(module D.Jlist(Goal))
begin fun marker ->
let open Printer_tag in
let has_marker g =
let is_marker = Localizable.equal marker in
let in_stmt = match g.Wpo.po_formula.source with
| Some(stmt,_) -> is_marker @@ localizable_of_stmt stmt
| None -> false
in
in_stmt ||
match WpPropId.property_of_id g.Wpo.po_pid with
| IPOther {io_loc = OLStmt(_,s)} -> is_marker @@ localizable_of_stmt s
| ip -> is_marker @@ Printer_tag.PIP ip
in
let select g = has_marker g && not @@ Wpo.is_tactic g in
let l = ref [] in
Wpo.iter_on_goals(fun g -> if select g then l := g :: !l) ;
List.sort Wpo.S.compare !l
end
let () =
R.register ~package ~kind:`EXEC ~name:"generateRTEGuards"
~descr:(Md.plain "Generate RTE guards for the function")
~input:(module AST.Marker)
~output:(module D.Junit)
begin function
| PVDecl (Some kf, _, _) ->
let setup = Factory.parse (Wp_parameters.Model.get ()) in
let driver = Driver.load_driver () in
let model = Factory.instance setup driver in
WpRTE.generate model kf
| _ -> ()
end
module Initialized_proxy = struct
type t =
| Only of Kernel_function.Set.t
| Except of Kernel_function.Set.t
type elem = All | Kf of Cil_types.kernel_function
type init = Add of elem | Remove of elem
let action set elem =
match elem, set with
| Add All, _ -> Except Kernel_function.Set.empty
| Remove All, _ -> Only Kernel_function.Set.empty
| Add (Kf kf), Except set ->
Except (Kernel_function.Set.remove kf set)
| Add (Kf kf), Only set ->
Only (Kernel_function.Set.add kf set)
| Remove (Kf kf), Except set ->
Except (Kernel_function.Set.add kf set)
| Remove (Kf kf), Only set ->
Only (Kernel_function.Set.remove kf set)
let parse name =
let add e = Add e and rem e = Remove e in
if String.equal name "@default"
|| String.equal name "+@default"
|| String.equal name "-@default"
then None
else if String.equal name "@all"
|| String.equal name "+@all"
then Some (Add All)
else if String.equal name "-@all"
then Some (Remove All)
else if String.starts_with ~prefix:"-" name
|| String.starts_with ~prefix:"+" name
then
let op = if String.get name 0 = '+' then add else rem in
let name = String.sub name 1 ((String.length name) -1 ) in
Some (op (Kf (Globals.Functions.find_by_name name)))
else
Some (Add (Kf (Globals.Functions.find_by_name name)))
let parse_action l s =
match parse s with
| None -> l
| Some value -> action l value
let pp_actions fmt actions =
let only, elements = match actions with
| Only set -> true, Kernel_function.Set.elements set
| Except set -> false, Kernel_function.Set.elements set
in
let pp fmt kf =
if only
then Kernel_function.pretty fmt kf
else Format.fprintf fmt "-%a" Kernel_function.pretty kf
in
Format.fprintf fmt "%s%a"
(if only then ""
else if elements = [] then "@all"
else "@all,")
(Pretty_utils.pp_list ~sep:"," pp) elements
let current_init_proxy =
ref (Only Kernel_function.Set.empty)
let hooks = ref []
let add_hook_on_update hook = hooks := hook :: !hooks
let set_init_proxy value =
current_init_proxy := value ;
List.iter (fun hook -> hook ()) !hooks
let update_init_proxy () =
ignore (RteGen.Options.DoInitialized.get ());
let line = RteGen.Options.DoInitialized.As_string.get () in
let entries = List.map String.trim @@ String.split_on_char ',' line in
let actions =
List.fold_left parse_action (Only Kernel_function.Set.empty) entries in
set_init_proxy actions
let () =
RteGen.Options.DoInitialized.add_set_hook
(fun _ _ -> update_init_proxy ())
let set actions =
RteGen.Options.DoInitialized.As_string.set
(Format.asprintf "%a" pp_actions actions) ;
set_init_proxy actions
let get () =
!current_init_proxy
end
module JInitialized_proxy =
struct
module Decl_list = D.Jlist(D.Jpair(AST.Decl)(D.Jstring))
type t = Initialized_proxy.t
let jtype =
D.declare ~package ~name:"initializedProxy" @@
Jrecord [ "only", Jboolean ; "elems", Decl_list.jtype]
let to_json s =
let only, set = match s with
| Initialized_proxy.Only set -> true, set
| Initialized_proxy.Except set -> false, set
in
let elems =
List.map
(fun kf -> Printer_tag.SFunction kf, Kernel_function.get_name kf)
(Kernel_function.Set.elements set)
in
`Assoc [
"only", `Bool only ;
"elems", Decl_list.to_json elems
]
let of_json json =
let = function
| Printer_tag.SFunction kf, _ -> kf
| _ -> raise Not_found
in
try
match Json.assoc json with
| [ (_, only) ; (_, elems) ] ->
let only = Json.bool only in
let elems = Decl_list.of_json elems in
let kfs = List.map extract_function elems in
let kfs = Kernel_function.Set.of_list kfs in
if only then Initialized_proxy.Only kfs else Except kfs
| _ -> raise Not_found
with _ ->
Wp_parameters.fatal "Cannot parse: %a" Json.pp json
end
let () =
ignore @@ S.register_state ~package ~name:"initialized"
~descr:(Md.plain "Configured properties filter")
~data:(module JInitialized_proxy)
~get:Initialized_proxy.get
~set:Initialized_proxy.set
~add_hook:Initialized_proxy.add_hook_on_update
()
let () =
ignore @@ S.register_state ~package ~name:"filter"
~descr:(Md.plain "Configured properties filter")
~data:(module D.Jlist(D.Jstring))
~get:Wp_parameters.Properties.get
~set:Wp_parameters.Properties.set
~add_hook:(fun f -> Wp_parameters.Properties.add_set_hook (fun _ -> f))
()
let is_call stmt =
match stmt.Cil_types.skind with
| Instr (Call _) | Instr (Local_init (_, ConsInit _, _)) -> true
| _ -> false
let start_proofs_marker = function
| Printer_tag.PExp _ | PTermLval _ | PLval _
| PGlobal _ | PType _ | PVDecl (None, _, _) ->
()
| PStmtStart (_, stmt) | PStmt (_, stmt) when is_call stmt ->
VC.command @@ VC.generate_call stmt
| PStmtStart (kf, stmt) | PStmt (kf, stmt) ->
let fold_ips _ ca bag =
let ids = WpPropId.mk_code_annot_ids kf stmt ca in
let props = Bag.ulist @@
List.map VC.generate_ip @@
List.map WpPropId.property_of_id ids
in
Bag.concat bag props
in
VC.command @@ Annotations.fold_code_annot fold_ips stmt Bag.empty
| PVDecl (Some kf, _, _) ->
VC.command @@ VC.generate_kf kf
| PIP property ->
VC.command @@ VC.generate_ip property
let () =
R.register ~package ~kind:`EXEC ~name:"startProofs"
~descr:(Md.plain "Generate goals and run provers")
~input:(module D.Joption(AST.Marker))
~output:(module D.Junit)
begin function
| None -> VC.command @@ VC.generate_all ()
| Some marker -> start_proofs_marker marker
end
let () =
R.register ~package ~kind:`EXEC ~name:"clearProofs"
~descr:(Md.plain "Clear goals")
~input:(module D.Junit)
~output:(module D.Junit)
begin fun () ->
Emitter.clear WpReached.emitter ;
CfgInfos.clear ();
Wpo.iter_on_goals
(fun g ->
let emitter = WpContext.get_emitter g.po_model in
Emitter.clear emitter) ;
Wpo.iter_on_goals Wpo.clear_results ;
Wpo.clear ();
end
let serverActivity = R.signal ~package
~name:"serverActivity"
~descr:(Md.plain "Proof Server Activity")
let () =
let server_sig = R.signature ~input:(module D.Junit) () in
let set_procs = R.result server_sig
~name:"procs" ~descr:(Md.plain "Max parallel tasks") (module D.Jint) in
let set_active = R.result server_sig
~name:"active" ~descr:(Md.plain "Active tasks") (module D.Jint) in
let set_done = R.result server_sig
~name:"done" ~descr:(Md.plain "Finished tasks") (module D.Jint) in
let set_todo = R.result server_sig
~name:"todo" ~descr:(Md.plain "Remaining jobs") (module D.Jint) in
R.register_sig ~package ~kind:`GET ~name:"getScheduledTasks"
~descr:(Md.plain "Scheduled tasks in proof server")
~signals:[serverActivity]
server_sig
begin
let monitored = ref false in
fun rq () ->
let server = ProverTask.server () in
if not !monitored then
begin
monitored := true ;
let signal () = R.emit serverActivity in
Task.on_server_activity server signal ;
Task.on_server_start server signal ;
Task.on_server_stop server signal ;
end ;
set_procs rq (Task.get_procs server) ;
set_active rq (Task.running server) ;
set_done rq (Task.terminated server) ;
set_todo rq (Task.remaining server) ;
end
let () = R.register ~package ~kind:`SET ~name:"cancelProofTasks"
~descr:(Md.plain "Cancel all scheduled proof tasks")
~input:(module D.Junit) ~output:(module D.Junit)
(fun () -> let server = ProverTask.server () in Task.cancel_all server)