Source file wpReport.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
let ladder = [| 1.0 ; 2.0 ; 3.0 ; 5.0 ; 10.0 ; 15.0 ;
20.0 ; 30.0 ; 40.0 ;
60.0 ; 90.0 ; 120.0 ; 180.0 ;
300.0 ; 600.0 ; 900.0 ; 1800.0 ;
3600.0 |]
let n0 = 16
let d0 = 4
let a0 = n0 * d0
let ak k = a0 lsl k - a0
let dk k = d0 lsl k
let range ?(limit=true) r =
let k = r / n0 in
let i = r mod n0 in
let a = ak k in
let d = dk k in
let i1 = if limit then i-1 else i in
let i2 = if limit then i+2 else i+1 in
max 1 (a + i1*d) , a + i2*d
let rank n =
let rec aux a k n =
let b = ak (succ k) - 1 in
if n <= b then
let d = dk k in
let i = (n-a) / d in
n0 * k + i
else aux b (succ k) n
in
let a = ak 0 in
if n < a then (-1) else aux a 0 n
type res = VALID | UNSUCCESS | INCONCLUSIVE | NORESULT
let result ~status ~smoke (r:VCS.result) =
match status with
| `Passed when smoke -> VALID
| _ ->
match r.VCS.verdict with
| VCS.NoResult | VCS.Computing _ -> NORESULT
| VCS.Failed -> INCONCLUSIVE
| VCS.Unknown | VCS.Timeout | VCS.Stepout | VCS.Invalid ->
if smoke then VALID else UNSUCCESS
| VCS.Valid ->
if smoke then UNSUCCESS else VALID
let best_result a b = match a,b with
| NORESULT,c | c,NORESULT -> c
| VALID,_ | _,VALID -> VALID
| UNSUCCESS,_ | _,UNSUCCESS -> UNSUCCESS
| INCONCLUSIVE,INCONCLUSIVE -> INCONCLUSIVE
type stats = {
mutable valid : int ;
mutable unsuccess : int ;
mutable inconclusive : int ;
mutable total : int ;
mutable steps : int ;
mutable time : float ;
mutable rank : int ;
}
let stats () = {
total=0 ; valid=0 ; unsuccess=0 ; inconclusive=0 ;
steps=0 ; rank=(-1) ; time=0.0 ;
}
let add_stat (r:res) (st:int) (tm:float) (s:stats) =
begin
s.total <- succ s.total ;
match r with
| VALID ->
if tm > s.time then s.time <- tm ;
if st > s.steps then s.steps <- st ;
s.valid <- succ s.valid
| NORESULT | UNSUCCESS -> s.unsuccess <- succ s.unsuccess
| INCONCLUSIVE -> s.inconclusive <- succ s.inconclusive
end
let add_qedstat (ts:float) (s:stats) =
if ts > s.time then s.time <- ts
let get_field js fd =
try Json.field fd js with Not_found | Invalid_argument _ -> `Null
let json_assoc fields =
let fields = List.filter (fun (_,d) -> d<>`Null) fields in
if fields = [] then `Null else `Assoc fields
let json_of_stats s =
let add fd v w = if v > 0 then (fd , `Int v)::w else w in
json_assoc
begin
add "total" s.total @@
add "valid" s.valid @@
add "failed" s.inconclusive @@
add "unknown" s.unsuccess @@
(if s.rank >= 0 then [ "rank" , `Int s.rank ] else [])
end
let rankify_stats s js =
let n = s.steps in
if n > 0 then
try
let r0 = Json.field "rank" js |> Json.int in
let a,b = range r0 in
if a <= n && n <= b then
s.rank <- r0
else
s.rank <- rank n
with Not_found | Invalid_argument _ ->
s.rank <- rank n
else
s.rank <- (-1)
type pstats = {
main : stats ;
prover : (VCS.prover,stats) Hashtbl.t ;
}
let pstats () = {
main = stats () ;
prover = Hashtbl.create 7 ;
}
let json_of_pstats p =
json_assoc
begin
Hashtbl.fold
(fun p s w ->
(VCS.name_of_prover p , json_of_stats s) :: w)
p.prover [ "wp:main" , json_of_stats p.main ]
end
let rankify_pstats p js =
begin
rankify_stats p.main (get_field js "wp:main") ;
Hashtbl.iter
(fun p s ->
rankify_stats s (get_field js @@ VCS.name_of_prover p) ;
) p.prover ;
end
let get_prover fs prover =
try Hashtbl.find fs.prover prover
with Not_found ->
let s = stats () in
Hashtbl.add fs.prover prover s ; s
let add_results ~status (plist:pstats list) (wpo:Wpo.t) =
let res = ref NORESULT in
let tm = ref 0.0 in
let sm = ref 0 in
let smoke = Wpo.is_smoke_test wpo in
List.iter
(fun (p,r) ->
let re = result ~status ~smoke r in
let st = r.VCS.prover_steps in
let tc = r.VCS.prover_time in
let ts = r.VCS.solver_time in
if re <> NORESULT then
begin
List.iter
(fun fs -> add_stat re st tc (get_prover fs p))
plist ;
if p <> VCS.Qed && ts > 0.0 then
List.iter
(fun fs -> add_qedstat ts (get_prover fs VCS.Qed))
plist ;
end ;
res := best_result !res re ;
if tc > !tm then tm := tc ;
if st > !sm then sm := st ;
) (Wpo.get_results wpo) ;
List.iter (fun fs -> add_stat !res !sm !tm fs.main) plist
type coverage = {
mutable covered : Property.Set.t ;
mutable proved : Property.Set.t ;
}
let coverage () = { covered = Property.Set.empty ; proved = Property.Set.empty }
let add_cover (s:coverage) ok p =
begin
s.covered <- Property.Set.add p s.covered ;
if ok then s.proved <- Property.Set.add p s.proved ;
end
type dstats = {
dstats : pstats ;
dcoverage : coverage ;
mutable dmap : pstats Property.Map.t ;
}
let dstats () = {
dstats = pstats () ;
dcoverage = coverage () ;
dmap = Property.Map.empty ;
}
let js_prop = Property.Names.get_prop_name_id
let json_of_dstats d =
json_assoc
begin
Property.Map.fold
(fun prop ps w ->
(js_prop prop , json_of_pstats ps) :: w)
d.dmap [ "wp:section" , json_of_pstats d.dstats ]
end
let rankify_dstats d js =
begin
rankify_pstats d.dstats (get_field js "wp:section") ;
Property.Map.iter
(fun prop ps ->
rankify_pstats ps (get_field js @@ js_prop prop)
) d.dmap ;
end
type entry =
| Axiom of string
| Fun of Kernel_function.t
let decode_chapter= function
| Axiom _ -> "axiomatic"
| Fun _ -> "function"
module Smap = Map.Make
(struct
type t = entry
let compare s1 s2 =
match s1 , s2 with
| Axiom a , Axiom b -> String.compare a b
| Axiom _ , Fun _ -> (-1)
| Fun _ , Axiom _ -> 1
| Fun f , Fun g -> Kernel_function.compare f g
end)
type fcstat = {
global : pstats ;
gcoverage : coverage ;
mutable dsmap : dstats Smap.t ;
}
let json_of_fcstat (fc : fcstat) =
begin
let functions = ref [] in
let axiomatics = ref [] in
Smap.iter
(fun entry ds ->
let acc , key = match entry with
| Axiom a -> axiomatics , a
| Fun kf -> functions , Kernel_function.get_name kf
in
acc := ( key , json_of_dstats ds ) :: !acc ;
) fc.dsmap ;
json_assoc [
"wp:global" , json_of_pstats fc.global ;
"wp:axiomatics" , json_assoc (List.rev (!axiomatics)) ;
"wp:functions" , json_assoc (List.rev (!functions)) ;
] ;
end
let rankify_fcstat fc js =
begin
rankify_pstats fc.global (get_field js "wp:global") ;
let jfunctions = get_field js "wp:functions" in
let jaxiomatics = get_field js "wp:axiomatics" in
Smap.iter
(fun entry ds ->
let js = match entry with
| Axiom a -> get_field jaxiomatics a
| Fun kf -> get_field jfunctions (Kernel_function.get_name kf)
in rankify_dstats ds js
) fc.dsmap ;
end
let get_section gs s =
try Smap.find s gs.dsmap
with Not_found ->
let ds = dstats () in
gs.dsmap <- Smap.add s ds gs.dsmap ; ds
let get_property ds p =
try Property.Map.find p ds.dmap
with Not_found ->
let ps = pstats () in
ds.dmap <- Property.Map.add p ps ds.dmap ; ps
let add_goal (gs:fcstat) wpo =
begin
let section = match Wpo.get_index wpo with
| Wpo.Axiomatic None -> Axiom ""
| Wpo.Axiomatic (Some a) -> Axiom a
| Wpo.Function(kf,_) -> Fun kf
in
let ds : dstats = get_section gs section in
let status,prop = Wpo.get_proof wpo in
let ps : pstats = get_property ds prop in
add_results ~status [gs.global ; ds.dstats ; ps] wpo ;
let ok = (status = `Passed) in
add_cover gs.gcoverage ok prop ;
add_cover ds.dcoverage ok prop ;
end
let fcstat () =
let fcstat : fcstat = {
global = pstats () ;
gcoverage = coverage () ;
dsmap = Smap.empty ;
} in
Wpo.iter ~on_goal:(add_goal fcstat) () ;
fcstat
type istat = {
fcstat: fcstat;
chapters : (string * (entry * dstats) list) list;
}
(** start chapter stats *)
let start_stat4chap fcstat =
let chapter = ref "" in
let decode_chapter e =
let code = decode_chapter e in
let is_new_code = (code <> !chapter) in
if is_new_code then
chapter := code;
is_new_code
in
let close_chapter (na,ca,ga) =
if ca = [] then !chapter,[],ga
else !chapter,[],((na,List.rev ca)::ga)
in
let (_,_,ga) =
let acc =
Smap.fold
(fun entry ds acc ->
let is_new_chapter = decode_chapter entry in
let (na,ca,ga) = if is_new_chapter
then close_chapter acc
else acc in
na,((entry,ds)::ca),ga
) fcstat.dsmap ("",[],[])
in if !chapter <> "" then close_chapter acc
else acc
in if ga = [] then None
else Some { fcstat = fcstat;
chapters = List.rev ga;
}
(** next chapters stats *)
let next_stat4chap istat =
match istat.chapters with
| ([] | _::[]) -> None
| _::l -> Some { istat with chapters = l }
type cistat = {
cfcstat: fcstat;
chapter : string;
sections : (entry * dstats) list;
}
(** start section stats of a chapter*)
let start_stat4sect istat =
match istat.chapters with
| [] -> None
| (c,s)::_ -> Some { cfcstat = istat.fcstat;
chapter = c;
sections = s;
}
(** next section stats *)
let next_stat4sect cistat =
match cistat.sections with
| ([] | _::[]) -> None
| _::l -> Some { cistat with sections = l }
type sistat = {
sfcstat: fcstat;
schapter : string ;
section : (entry * dstats);
properties : (Property.t * pstats) list;
}
(** start property stats of a section *)
let start_stat4prop cistat =
match cistat.sections with
| [] -> None
| ((_,ds) as s)::_ ->
Some { sfcstat = cistat.cfcstat;
schapter = cistat.chapter;
section = s;
properties = List.rev (Property.Map.fold
(fun p ps acc -> (p,ps)::acc) ds.dmap []);
}
(** next property stats *)
let next_stat4prop sistat =
match sistat.properties with
| ([] | _::[]) -> None
| _::l -> Some { sfcstat = sistat.sfcstat;
schapter = sistat.schapter;
section = sistat.section;
properties = l;
}
(** generic iterator *)
let iter_stat ?first ?sep ?last ~from start next=
if first<>None || sep<>None || last <> None then
let items = ref (start from) in
if !items <> None then
begin
let apply v = function
| None -> ()
| Some app -> app v
in
let next app =
let item = (Option.get !items) in
apply item app;
items := next item
in
next first;
if sep<>None || last <> None then
begin
while !items <> None do
next sep;
done;
apply () last;
end
end
type config = {
mutable status_passed : string ;
mutable status_failed : string ;
mutable status_inconclusive : string ;
mutable status_untried : string ;
mutable lemma_prefix : string ;
mutable axiomatic_prefix : string ;
mutable function_prefix : string ;
mutable property_prefix : string ;
mutable global_section: string ;
mutable axiomatic_section: string ;
mutable function_section : string ;
mutable console : bool ;
mutable zero : string ;
}
let pp_zero ~config fmt =
if config.console
then Format.fprintf fmt "%4s" config.zero
else Format.pp_print_string fmt config.zero
let percent ~config fmt number total =
if total <= 0 || number < 0
then pp_zero ~config fmt
else
if number >= total then
Format.pp_print_string fmt (if config.console then " 100" else "100")
else
let ratio = float_of_int number /. float_of_int total in
Format.fprintf fmt "%4.1f" (100.0 *. ratio)
let number ~config fmt k =
if k = 0
then pp_zero ~config fmt
else
if config.console
then Format.fprintf fmt "%4d" k
else Format.pp_print_int fmt k
let properties ~config fmt (s:coverage) = function
| "" -> percent ~config fmt (Property.Set.cardinal s.proved) (Property.Set.cardinal s.covered)
| "total" -> number ~config fmt (Property.Set.cardinal s.covered)
| "valid" -> number ~config fmt (Property.Set.cardinal s.proved)
| "failed" -> number ~config fmt (Property.Set.cardinal s.covered - Property.Set.cardinal s.proved)
| _ -> raise Exit
let is_stat_name = function
| "success"
| "total"
| "valid" | ""
| "failed"
| "status"
| "inconclusive"
| "unsuccess"
| "time"
| "perf"
| "steps"
| "range" -> true
| _ -> false
let stat ~config fmt s = function
| "success" -> percent ~config fmt s.valid s.total
| "total" -> number ~config fmt s.total
| "valid" | "" -> number ~config fmt s.valid
| "failed" -> number ~config fmt (s.unsuccess + s.inconclusive)
| "status" ->
let msg =
if s.inconclusive > 0 then config.status_inconclusive else
if s.unsuccess > 0 then config.status_failed else
if s.valid >= s.total then config.status_passed else
config.status_untried
in Format.pp_print_string fmt msg
| "inconclusive" -> number ~config fmt s.inconclusive
| "unsuccess" -> number ~config fmt s.unsuccess
| "time" ->
if s.time > 0.0 then
Rformat.pp_time_range ladder fmt s.time
| "perf" ->
if s.time > Rformat.epsilon then
Format.fprintf fmt "(%a)" Rformat.pp_time s.time
| "steps" ->
if s.steps > 0 then Format.fprintf fmt "(%d)" s.steps
| "range" ->
if s.rank >= 0 then
let a,b = range s.rank in
Format.fprintf fmt "(%d..%d)" a b
| _ -> raise Exit
let pstats ~config fmt s cmd arg =
match cmd with
| "wp" | "qed" -> stat ~config fmt (get_prover s VCS.Qed) arg
| cmd when is_stat_name cmd -> stat ~config fmt s.main cmd
| prover ->
match (VCS.parse_prover prover) with
| None -> Wp_parameters.error ~once:true "Unknown prover name %s" prover
| Some prover -> stat ~config fmt (get_prover s prover) arg
let pcstats ~config fmt (s,c) cmd arg =
match cmd with
| "prop" -> properties ~config fmt c arg
| _ -> pstats ~config fmt s cmd arg
let env_toplevel ~config gstat fmt cmd arg =
try
pcstats ~config fmt (gstat.global, gstat.gcoverage) cmd arg
with Exit ->
if arg=""
then Wp_parameters.error ~once:true "Unknown toplevel-format '%%%s'" cmd
else Wp_parameters.error ~once:true "Unknown toplevel-format '%%%s:%s'" cmd arg
let env_chapter chapter_name fmt cmd arg =
try
match cmd with
| "chapter" | "name" ->
Format.pp_print_string fmt chapter_name
| _ -> raise Exit
with Exit ->
if arg=""
then Wp_parameters.error ~once:true "Unknown chapter-format '%%%s'" cmd
else Wp_parameters.error ~once:true "Unknown chapter-format '%%%s:%s'" cmd arg
let env_section ~config ~name sstat fmt cmd arg =
try
let entry,ds = match sstat.sections with
| section_item::_others -> section_item
| _ -> raise Exit
in match cmd with
| "chapter" ->
let chapter = match entry with
| Axiom _ -> config.axiomatic_section
| Fun _ -> config.function_section
in Format.pp_print_string fmt chapter
| "name" | "section" | "global" | "axiomatic" | "function" ->
if cmd <> "name" && cmd <> "section" && name <> cmd then
Wp_parameters.error "Invalid section-format '%%%s' inside a section %s" cmd name;
let prefix,name = match entry with
| Axiom "" -> config.lemma_prefix,""
| Axiom a -> config.axiomatic_prefix,a
| Fun kf -> config.function_prefix, ( Kernel_function.get_name kf)
in Format.fprintf fmt "%s%s" prefix name
| _ ->
pcstats ~config fmt (ds.dstats, ds.dcoverage) cmd arg
with Exit ->
if arg=""
then Wp_parameters.error ~once:true "Unknown section-format '%%%s'" cmd
else Wp_parameters.error ~once:true "Unknown section-format '%%%s:%s'" cmd arg
let env_property ~config ~name pstat fmt cmd arg =
try
let entry = fst pstat.section in
let p,stat = match pstat.properties with
| property_item::_others -> property_item
| _ -> raise Exit
in match cmd with
| "chapter" ->
let chapter = match entry with
| Axiom _ -> config.axiomatic_section
| Fun _ -> config.function_section
in Format.pp_print_string fmt chapter
| "section" | "global" | "axiomatic" | "function" ->
if cmd <> "section" && name <> cmd then
Wp_parameters.error "Invalid property-format '%%%s' inside a section %s" cmd name;
let prefix,name = match entry with
| Axiom "" -> config.lemma_prefix,""
| Axiom a -> config.axiomatic_prefix,a
| Fun kf -> config.function_prefix, ( Kernel_function.get_name kf)
in Format.fprintf fmt "%s%s" prefix name
| "name" ->
Format.fprintf fmt "%s%s" config.property_prefix
(Property.Names.get_prop_name_id p)
| "property" ->
Description.pp_local fmt p
| _ ->
pstats ~config fmt stat cmd arg
with Exit ->
if arg=""
then Wp_parameters.error ~once:true "Unknown property-format '%%%s'" cmd
else Wp_parameters.error ~once:true "Unknown property-format '%%%s:%s'" cmd arg
let print_property (pstat:sistat) ~config ~name ~prop fmt =
Rformat.pretty (env_property ~config ~name pstat) fmt prop
let print_section (sstat:cistat) ~config ~name ~sect ~prop fmt =
if sect <> "" then
Rformat.pretty (env_section ~config ~name sstat) fmt sect ;
if prop <> "" then
let print_property pstat = print_property pstat ~config ~name ~prop fmt
in iter_stat ~first:print_property ~sep:print_property ~from:sstat start_stat4prop next_stat4prop
let print_chapter (cstat:istat) ~config ~chap ~sect ~glob ~axio ~func ~prop fmt =
let chapter_item = match cstat.chapters with
| chapter_item::_others -> chapter_item
| _ -> raise Exit
in let section_name = fst chapter_item
in let section,chapter_name = match section_name with
| "global" -> glob,config.global_section
| "axiomatic" -> axio,config.axiomatic_section
| "function" -> func,config.function_section
| _ -> sect,""
in let section,section_name = if section <> "" then section,section_name else sect,""
in
if chap <> "" then
Rformat.pretty (env_chapter chapter_name) fmt chap ;
if section <> "" || prop <> "" then
let print_section sstat = print_section sstat ~config ~name:section_name ~sect:section ~prop fmt
in iter_stat ~first:print_section ~sep:print_section ~from:cstat start_stat4sect next_stat4sect
let print gstat ~config ~head ~tail ~chap ~sect ~glob ~axio ~func ~prop fmt =
begin
if head <> "" then
Rformat.pretty (env_toplevel ~config gstat) fmt head ;
if chap <> "" || sect <> "" || glob <> "" || axio <> "" || func <> "" || prop <> "" then
let print_chapter cstat = print_chapter cstat ~config ~chap ~sect ~glob ~axio ~func ~prop fmt
in iter_stat ~first:print_chapter ~sep:print_chapter ~from:gstat start_stat4chap next_stat4chap ;
if tail <> "" then
Rformat.pretty (env_toplevel ~config gstat) fmt tail ;
end
type section = END | HEAD | TAIL
| CHAPTER
| SECTION | GLOB_SECTION | AXIO_SECTION | FUNC_SECTION
| PROPERTY
let export gstat specfile =
let config = {
console = false ;
zero = "-" ;
status_passed = " Ok " ;
status_failed = "Failed" ;
status_inconclusive = "*Bug**" ;
status_untried = " " ;
lemma_prefix = "Lemma " ;
axiomatic_prefix = "Axiomatic " ;
function_prefix = "" ;
property_prefix = "" ;
global_section = "Globals" ;
axiomatic_section = "Axiomatics" ;
function_section = "Functions" ;
} in
let head = Buffer.create 64 in
let tail = Buffer.create 64 in
let chap = Buffer.create 64 in
let sect = Buffer.create 64 in
let glob = Buffer.create 64 in
let axio = Buffer.create 64 in
let func = Buffer.create 64 in
let sect_prop = Buffer.create 64 in
let file = ref None in
let section = ref HEAD in
begin
let cin = open_in specfile in
try
while true do
let line = input_line cin in
match Rformat.command line with
| Rformat.ARG("AXIOMATIC_PREFIX",f) -> config.axiomatic_prefix <- f
| Rformat.ARG("FUNCTION_PREFIX",f) -> config.function_prefix <- f
| Rformat.ARG("PROPERTY_PREFIX",f) -> config.property_prefix <- f
| Rformat.ARG("LEMMA_PREFIX",f) -> config.lemma_prefix <- f
| Rformat.ARG("GLOBAL_SECTION",f) -> config.global_section <- f
| Rformat.ARG("AXIOMATIC_SECTION",f) -> config.axiomatic_section <- f
| Rformat.ARG("FUNCTION_SECTION",f) -> config.function_section <- f
| Rformat.ARG("PASSED",s) -> config.status_passed <- s
| Rformat.ARG("FAILED",s) -> config.status_failed <- s
| Rformat.ARG("INCONCLUSIVE",s) -> config.status_inconclusive <- s
| Rformat.ARG("UNTRIED",s) -> config.status_untried <- s
| Rformat.ARG("ZERO",z) -> config.zero <- z
| Rformat.ARG("FILE",f) -> file := Some f
| Rformat.ARG("SUFFIX",e) ->
let basename = Wp_parameters.ReportName.get () in
let filename = basename ^ e in
file := Some filename
| Rformat.CMD "CONSOLE" -> config.console <- true
| Rformat.CMD "END" -> section := END
| Rformat.CMD "HEAD" -> section := HEAD
| Rformat.CMD "TAIL" -> section := TAIL
| Rformat.CMD "CHAPTER" -> section := CHAPTER
| Rformat.CMD "SECTION" -> section := SECTION
| Rformat.CMD "GLOBAL" -> section := GLOB_SECTION
| Rformat.CMD "AXIOMATIC" -> section := AXIO_SECTION
| Rformat.CMD "FUNCTION" -> section := FUNC_SECTION
| Rformat.CMD "PROPERTY" -> section := PROPERTY
| Rformat.CMD a | Rformat.ARG(a,_) ->
Wp_parameters.error "Report '%s': unknown command '%s'" specfile a
| Rformat.TEXT ->
if !section <> END then
let text = match !section with
| HEAD -> head
| CHAPTER -> chap
| SECTION -> sect
| GLOB_SECTION -> glob
| AXIO_SECTION -> axio
| FUNC_SECTION -> func
| PROPERTY -> sect_prop
| TAIL|END -> tail
in
Buffer.add_string text line ;
Buffer.add_char text '\n' ;
done
with
| End_of_file -> close_in cin
| err -> close_in cin ; raise err
end ;
match !file with
| None ->
Log.print_on_output
(print gstat ~config
~head:(Buffer.contents head) ~tail:(Buffer.contents tail)
~chap:(Buffer.contents chap)
~sect:(Buffer.contents sect)
~glob:(Buffer.contents glob)
~axio:(Buffer.contents axio)
~func:(Buffer.contents func)
~prop:(Buffer.contents sect_prop))
| Some report ->
Wp_parameters.feedback "Report '%s'" report ;
let cout = open_out report in
let fout = Format.formatter_of_out_channel cout in
try
print gstat ~config
~head:(Buffer.contents head) ~tail:(Buffer.contents tail)
~chap:(Buffer.contents chap)
~sect:(Buffer.contents sect)
~glob:(Buffer.contents glob)
~axio:(Buffer.contents axio)
~func:(Buffer.contents func)
~prop:(Buffer.contents sect_prop)
fout ;
Format.pp_print_flush fout () ;
close_out cout ;
with err ->
Format.pp_print_flush fout () ;
close_out cout ;
raise err
let export_json gstat ?jinput ~joutput () =
begin
let js =
try
let jfile = match jinput with
| None ->
Wp_parameters.feedback "Report '%s'" joutput ;
joutput
| Some jinput ->
Wp_parameters.feedback "Report in: '%s'" jinput ;
Wp_parameters.feedback "Report out: '%s'" joutput ;
jinput
in
let jpath = Filepath.Normalized.of_string jfile in
if Filepath.exists jpath then
Json.load_file jpath
else `Null
with Json.Error(file,line,msg) ->
let source = Log.source ~file ~line in
Wp_parameters.error ~source "Incorrect json file: %s" msg ;
`Null
in
rankify_fcstat gstat js ;
Json.save_file (Filepath.Normalized.of_string joutput) (json_of_fcstat gstat) ;
end