Source file wpPropId.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
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
1112
1113
1114
1115
1116
1117
1118
1119
1120
1121
1122
1123
1124
1125
1126
1127
1128
1129
1130
1131
1132
1133
1134
1135
1136
1137
1138
1139
1140
1141
1142
1143
1144
1145
1146
1147
1148
1149
1150
1151
1152
1153
1154
1155
1156
1157
1158
1159
1160
1161
1162
1163
1164
1165
1166
1167
1168
open Cil_types
open Cil_datatype
(** Beside the property identification, it can be found in different contexts
* depending on which part of the computation is involved.
* For instance, properties on loops are split in 2 parts : establishment and
* preservation.
*)
type prop_kind =
| PKTactic (** tactical sub-goal *)
| PKCheck (** internal check *)
| PKProp (** normal property *)
| PKEstablished (** computation related to a loop property before the loop. *)
| PKPreserved (** computation related to a loop property inside the loop. *)
| PKPropLoop (** loop property used as hypothesis inside a loop. *)
| PKVarDecr (** computation related to the decreasing of a variant in a loop *)
| PKVarPos (** computation related to a loop variant being positive *)
| PKVarRel (** computation related to a generalized loop variant *)
| PKAFctOut (** computation related to the function assigns on normal termination *)
| PKAFctExit (** computation related to the function assigns on exit termination *)
| PKTerminates (** computation related to the termination *)
| PKDecreases (** computation related to the decreases clause *)
| PKSmoke (** expected to fail *)
| PKPre of kernel_function * stmt * Property.t
(** precondition for function
at stmt, property of the require. Many information that should come
from the p_prop part of the prop_id, but in the PKPre case,
it seems that it is hidden in a IPBlob property ! *)
type prop_id = {
p_kind : prop_kind ;
p_prop : Property.t ;
p_doomed : Property.t list ;
p_unreachable : Property.other_loc ;
p_part : (int * int) option ;
}
let unknown = Property.OLGlob Cil_datatype.Location.unknown
let tactical ~gid =
let ip = "Wp.Tactical." ^ gid in
{ p_kind = PKTactic ;
p_prop = Property.(ip_other ip unknown);
p_doomed = [] ;
p_unreachable = unknown ;
p_part = None }
let parts_of_id p = p.p_part
let property_of_id p = p.p_prop
let doomed_if_valid p = p.p_doomed
let unreachable_if_valid p = p.p_unreachable
let mk_part pid (k, n) = { pid with p_part = Some (k,n) }
let source_of_id p = fst (Property.location p.p_prop)
exception Found of int
let num_of_bhv_from bhv (out, _) =
match bhv.b_assigns with
WritesAny -> Wp_parameters.fatal "no \\from in this behavior ???"
| Writes l ->
let add n (o, f) = match f with FromAny -> n
| From _ ->
if Logic_utils.is_same_identified_term out o then
raise (Found n)
else n+1
in
try
let _ = List.fold_left add 1 l in
Wp_parameters.fatal "didn't found this \\from"
with Found n -> n
let mk_prop kind prop =
{ p_kind=kind; p_prop=prop; p_unreachable=unknown; p_doomed=[]; p_part=None }
let mk_check prop = mk_prop PKCheck prop
let mk_property prop = mk_prop PKProp prop
let mk_annot_id kf stmt ca = Property.ip_of_code_annot_single kf stmt ca
let mk_annot_ids kf stmt ca = Property.ip_of_code_annot kf stmt ca
let mk_code_annot_ids kf s ca = List.map (mk_prop PKProp) (mk_annot_ids kf s ca)
let mk_assert_id kf s ca = mk_prop PKProp (mk_annot_id kf s ca)
let mk_loop_inv_id kf s ~established ca =
let kind = if established then PKEstablished else PKPreserved in
mk_prop kind (mk_annot_id kf s ca)
let mk_loop_inv kf s ca =
mk_loop_inv_id kf s ~established:true ca,
mk_loop_inv_id kf s ~established:false ca
let mk_inv_hyp_id kf s ca = mk_prop PKPropLoop (mk_annot_id kf s ca)
let mk_var_decr_id kf s ca = mk_prop PKVarDecr (mk_annot_id kf s ca)
let mk_var_pos_id kf s ca = mk_prop PKVarPos (mk_annot_id kf s ca)
let mk_var_id kf s ca = mk_prop PKVarRel (mk_annot_id kf s ca)
let mk_loop_from_id kf s ca from =
let id = Property.ip_of_from kf (Kstmt s) (Property.Id_loop ca) from in
mk_prop PKPropLoop (Option.get id)
let mk_bhv_from_id kf ki a bhv from =
let a = Datatype.String.Set.of_list a in
let id = Property.ip_of_from kf ki (Property.Id_contract (a,bhv)) from in
mk_prop PKProp (Option.get id)
let get_kind_for_tk tkind has_exit = match tkind with
| Normal ->
if has_exit then PKAFctOut else PKProp
| Exits -> PKAFctExit
| _ -> assert false
let mk_fct_from_id kf kf_has_exit bhv tkind from =
let contract_info = Property.Id_contract(Datatype.String.Set.empty,bhv) in
let id = Property.ip_of_from kf Kglobal contract_info from in
let kind = get_kind_for_tk tkind kf_has_exit in
mk_prop kind (Option.get id)
let mk_disj_bhv_id (kf,ki,active,disj) =
mk_prop PKProp (Property.ip_of_disjoint kf ki ~active disj)
let mk_compl_bhv_id (kf,ki,active,comp) =
mk_prop PKProp (Property.ip_of_complete kf ki ~active comp)
let mk_decrease_id kf s x =
mk_prop PKDecreases (Property.ip_of_decreases kf s x)
let mk_lemma_id l = mk_prop PKProp (LogicUsage.ip_lemma l)
let mk_stmt_assigns_id kf s active b a =
let active = Datatype.String.Set.of_list active in
let b = Property.Id_contract (active,b) in
let p = Property.ip_of_assigns kf (Kstmt s) b (Writes a) in
Option.map (mk_prop PKProp) p
let mk_loop_assigns_id kf s ca a =
let ca = Property.Id_loop ca in
let p = Property.ip_of_assigns kf (Kstmt s) ca (Writes a) in
Option.map (mk_prop PKPropLoop) p
let mk_fct_assigns_id kf kf_has_exit b tkind a =
let b = Property.Id_contract(Datatype.String.Set.empty,b) in
let kind = get_kind_for_tk tkind kf_has_exit in
let p = Property.ip_of_assigns kf Kglobal b (Writes a) in
Option.map (mk_prop kind) p
let mk_pre_id kf ki b p =
mk_prop PKProp (Property.ip_of_requires kf ki b p)
let mk_post_id kf ki b p =
mk_prop PKProp (Property.ip_of_ensures kf ki b p)
let mk_terminates_id kf kinstr p =
mk_prop PKTerminates (Property.ip_of_terminates kf kinstr p)
let mk_stmt_post_id kf s b p =
mk_prop PKProp (Property.ip_of_ensures kf (Kstmt s) b p)
let mk_fct_post_id kf b p =
mk_prop PKProp (Property.ip_of_ensures kf Kglobal b p)
let mk_call_pre_id called_kf s_call called_pre called_pre_p =
let kind = PKPre (called_kf, s_call, called_pre) in
mk_prop kind called_pre_p
let mk_smoke kf ~id ?(doomed=[]) ?unreachable () =
let oloc = match unreachable with
| None -> Property.OLContract kf
| Some stmt -> Property.OLStmt(kf,stmt)
in {
p_kind = PKSmoke;
p_prop = Property.ip_other ("wp_smoke_" ^id) oloc ;
p_doomed = doomed ;
p_unreachable = oloc ;
p_part = None ;
}
let kind_order = function
| PKProp -> 0
| PKPre _ -> 1
| PKEstablished -> 2
| PKPreserved -> 3
| PKVarPos -> 4
| PKVarDecr -> 5
| PKVarRel -> 6
| PKPropLoop -> 7
| PKAFctOut -> 8
| PKAFctExit -> 9
| PKCheck -> 10
| PKTactic -> 11
| PKSmoke -> 12
| PKTerminates -> 13
| PKDecreases -> 14
let compare_kind k1 k2 = match k1, k2 with
PKPre (kf1, ki1, p1), PKPre (kf2, ki2, p2) ->
let cmp = Kernel_function.compare kf1 kf2 in
if cmp <> 0 then cmp
else
let cmp = Stmt.compare ki1 ki2 in
if cmp <> 0 then cmp
else
Property.compare p1 p2
| _,_ -> Stdlib.compare (kind_order k1) (kind_order k2)
let compare_prop_id pid1 pid2 =
let p1 = property_of_id pid1 in
let p2 = property_of_id pid2 in
let cmp = Description.full_compare p1 p2 in
if cmp <> 0 then cmp
else
let cmp = compare_kind pid2.p_kind pid1.p_kind in
if cmp <> 0 then cmp
else
Stdlib.compare pid1.p_part pid2.p_part
module PropIdRaw =
Datatype.Make_with_collections(
struct
type t = prop_id
include Datatype.Undefined
let name = "WpAnnot.prop_id"
let reprs = List.map mk_property Property.reprs
let hash pid = Property.hash pid.p_prop
let compare = compare_prop_id
let equal pid1 pid2 = compare_prop_id pid1 pid2 = 0
let copy = Datatype.undefined
let rehash = Datatype.identity
let pretty = Datatype.undefined
let mem_project = Datatype.never_any_project
end)
module NameUniquify(D:Datatype.S_with_collections)(S:sig
val name: string
val basename: D.t -> string
end) :
sig
val unique_basename: D.t -> string
end
=
struct
module NamesTbl = State_builder.Hashtbl(Datatype.String.Hashtbl)(Datatype.Int)
(struct
let name = S.name^"Names"
let dependencies = [ ]
let size = 97
end)
module IndexTbl =
State_builder.Hashtbl(D.Hashtbl)(Datatype.String)
(struct
let name = S.name^"Index"
let dependencies =
[ Ast.self;
NamesTbl.self;
Globals.Functions.self;
Annotations.code_annot_state;
Annotations.funspec_state;
Annotations.global_state ]
let size = 97
end)
(** returns the name that should be returned by the function [get_prop_name_id]
if the given property has [name] as basename. That name is reserved so that
[get_prop_name_id prop] can never return an identical name. *)
let reserve_name_id pid =
let basename = S.basename pid in
try
let speed_up_start = NamesTbl.find basename in
let n,unique_name = Extlib.make_unique_name NamesTbl.mem ~sep:"_" ~start:speed_up_start basename
in NamesTbl.replace basename (succ n) ;
unique_name
with Not_found ->
NamesTbl.add basename 2 ;
basename
(** returns a unique name identifying the property.
This name is built from the basename of the property. *)
let unique_basename pid =
try IndexTbl.find pid
with Not_found ->
let unique_name = reserve_name_id pid in
IndexTbl.add pid unique_name ;
unique_name
end
module Names:
sig
val get_prop_id_name: prop_id -> string
end =
struct
(** Uniquify the first part of the prop_id *)
module Uniquify1 = NameUniquify(Property)(struct
let name = "Wp.WpPropId.Names."
let basename ip =
let truncate = max 20 (Wp_parameters.TruncPropIdFileName.get ()) in
Property.Names.get_prop_basename ~truncate ip
end)
let get_ip ip =
Uniquify1.unique_basename ip
(** Uniquify call-site for precondition check. So
that precondition of the same call-site are grouped *)
module CallSite = Datatype.Triple_with_collections
(Kernel_function)(Kernel_function)(Stmt)
(struct let module_name = "Wp.WpPropId.CallSite" end)
module Uniquify_Stmt = NameUniquify(CallSite)(struct
let name = "Wp.WpPropId.Names3."
let basename (caller_kf,callee_kf,_stmt) =
(Kernel_function.get_name caller_kf)^"_call_"^(Kernel_function.get_name callee_kf)
end)
let get_prop_id_base p =
match p.p_kind , p.p_prop with
| PKEstablished , p -> get_ip p ^ "_established"
| PKPreserved , p -> get_ip p ^ "_preserved"
| PKVarDecr , p -> get_ip p ^ "_decrease"
| PKVarPos , p -> get_ip p ^ "_positive"
| PKVarRel , p -> get_ip p ^ "_relation"
| PKAFctOut , p -> get_ip p ^ "_normal"
| PKAFctExit , p -> get_ip p ^ "_exit"
| PKPre(callee_kf,stmt,pre) , _ ->
let caller_kf = Kernel_function.find_englobing_kf stmt in
let call_string =
Uniquify_Stmt.unique_basename (caller_kf,callee_kf,stmt)
in
let ip_string = get_ip pre in
let ip_string =
Option.value ~default:ip_string
(Extlib.string_del_prefix
((Kernel_function.get_name callee_kf)^"_")
ip_string)
in
call_string^"_"^ip_string
| _ , p ->
get_ip p
let get_prop_id_basename p =
let basename = get_prop_id_base p in
match p.p_part with
| None -> basename
| Some(k,n) ->
if n < 10 then Printf.sprintf "%s_part%d" basename (succ k) else
if n < 100 then Printf.sprintf "%s_part%02d" basename (succ k) else
if n < 1000 then Printf.sprintf "%s_part%03d" basename (succ k) else
Printf.sprintf "%s_part%06d" basename (succ k)
module Uniquify2 = NameUniquify(PropIdRaw)(struct
let name = "Wp.WpPropId.Names2."
let basename = get_prop_id_basename
end)
let get_prop_id_name p =
Uniquify2.unique_basename p
end
let get_propid = Names.get_prop_id_name
(** Name related to a property PO *)
let pp_propid fmt pid =
Format.pp_print_string fmt (get_propid pid)
let pp_names fmt l =
let l = Datatype.String.Set.elements l in
match l with
| [] -> ()
| _ -> Format.fprintf fmt "_%a" (Wp_error.pp_string_list ~empty:"" ~sep:"_") l
let ident_names names =
List.filter (function "" -> true
| _ as n -> '\"' <> (String.get n 0) ) names
let user_pred_names p =
let p_names = ident_names p.tp_statement.pred_name in
if p.tp_kind = Check then "@check"::p_names else p_names
let code_annot_names ca = match ca.annot_content with
| AAssert (_, pred) -> "@assert" :: user_pred_names pred
| AInvariant (_,_,pred) -> "@invariant":: user_pred_names pred
| AVariant (term, _) -> "@variant"::(ident_names term.term_name)
| AExtended(_,_,{ext_name}) -> [Printf.sprintf "@%s" ext_name]
| _ -> []
(** This is used to give the name of the property that the user can give
* to select it from the command line (-wp-prop option) *)
let user_prop_names p =
let open Property in match p with
| IPPredicate {ip_kind; ip_pred} ->
Format.asprintf "@@%a" Property.pretty_predicate_kind ip_kind ::
user_pred_names ip_pred.ip_content
| IPExtended {ie_ext={ext_name}} -> [ Printf.sprintf "@%s" ext_name ]
| IPCodeAnnot {ica_ca} -> code_annot_names ica_ca
| IPComplete {ic_bhvs} ->
let kind_name = "@complete_behaviors" in
let name = Format.asprintf "complete_behaviors%a" pp_names ic_bhvs
in kind_name::[name]
| IPDisjoint {ic_bhvs} ->
let kind_name = "@disjoint_behaviors" in
let name = Format.asprintf "disjoint_behaviors%a" pp_names ic_bhvs
in kind_name::[name]
| IPAssigns {ias_froms} ->
List.fold_left
(fun acc (t,_) -> (ident_names t.it_content.term_name) @ acc)
["@assigns"] ias_froms
| IPDecrease {id_ca=Some ca} -> "@decreases"::code_annot_names ca
| IPDecrease _ -> [ "@decreases" ]
| IPLemma {il_name = a; il_pred = l} ->
let names = "@lemma"::a::user_pred_names l in
begin
match LogicUsage.section_of_lemma a with
| LogicUsage.Toplevel _ -> names
| LogicUsage.Axiomatic ax -> ax.LogicUsage.ax_name::names
end
| IPFrom _
| IPAllocation _
| IPAxiomatic _
| IPBehavior _
| IPReachable _
| IPPropertyInstance _
| IPTypeInvariant _
| IPGlobalInvariant _
| IPOther _ -> []
let user_bhv_names p =
let open Property in
let fors = match p with
| Property.IPCodeAnnot { ica_ca } ->
let fors = match ica_ca.annot_content with
| Cil_types.AAssert (fors, _)
| Cil_types.AStmtSpec (fors, _)
| Cil_types.AInvariant (fors, _, _)
| Cil_types.AAssigns (fors, _)
| Cil_types.AAllocation (fors, _)
| Cil_types.AExtended (fors, _, _) -> fors
| _ -> []
in fors
| _ -> []
in Option.fold ~none:fors ~some:(fun b -> b.b_name :: fors) (get_behavior p)
let string_of_termination_kind = function
Normal -> "ensures"
| Exits -> "exits"
| Breaks -> "breaks"
| Continues -> "continues"
| Returns -> "returns"
let label_of_kind = function
| PKTactic -> "Tactic"
| PKSmoke -> "Smoke-test"
| PKCheck -> "Check"
| PKProp -> "Property"
| PKPropLoop -> "Invariant"
| PKEstablished -> "Establishment"
| PKPreserved -> "Preservation"
| PKVarDecr -> "Decreasing"
| PKVarPos -> "Positive"
| PKVarRel -> "Relation"
| PKAFctOut -> "Function assigns"
| PKAFctExit -> "Exit assigns"
| PKTerminates -> "Terminates"
| PKDecreases -> "Decreases"
| PKPre(kf,_,_) ->
Printf.sprintf "Precondition for '%s'" (Kernel_function.get_name kf)
let label_of_prop_id p =
match p.p_part with
| None -> label_of_kind p.p_kind
| Some(k,n) ->
Printf.sprintf "%s (%d/%d)" (label_of_kind p.p_kind) (succ k) n
module Pretty =
struct
open Format
let pp_part fmt p = match p.p_part with
| None -> ()
| Some(k,n) -> fprintf fmt " (%d/%d)" (succ k) n
let pp_subprop fmt p = match p.p_kind with
| PKProp | PKTactic | PKCheck | PKPropLoop | PKSmoke
| PKTerminates | PKDecreases -> ()
| PKEstablished -> pp_print_string fmt " (established)"
| PKPreserved -> pp_print_string fmt " (preserved)"
| PKVarDecr -> pp_print_string fmt " (decrease)"
| PKVarPos -> pp_print_string fmt " (positive)"
| PKVarRel -> pp_print_string fmt " (relation)"
| PKAFctOut -> pp_print_string fmt " (return)"
| PKAFctExit -> pp_print_string fmt " (exit)"
| PKPre(kf,_,_) -> fprintf fmt " (call '%s')" (Kernel_function.get_name kf)
let pp_prop fmt p =
Description.pp_localized ~kf:`Never ~ki:false ~kloc:false fmt p.p_prop
let pp_local fmt p =
begin
pp_prop fmt p ;
pp_subprop fmt p ;
pp_part fmt p ;
end
end
let pretty_local = Pretty.pp_local
module PropId =
struct
include PropIdRaw
let pretty = pp_propid
end
type hints = {
mutable required : string list ;
mutable hints : string list ;
}
let add_hint hs x =
if not (List.mem x hs.hints) then hs.hints <- x :: hs.hints
let add_required hs x =
if not (List.mem x hs.required) then hs.required <- x :: hs.required
let stmt_hints hs s =
List.iter
(fun label ->
match label with
| Label(a,_,src) -> if src then add_hint hs a
| Default _ -> add_hint hs "default"
| Case(e,_) -> match Ctypes.get_int64 e with
| Some k -> add_hint hs ("case-" ^ Int64.to_string k)
| None -> ()
) s.labels
let kinstr_hints hs = function
| Kstmt s -> stmt_hints hs s
| Kglobal -> ()
let propid_hints hs p =
let open Property in
match p.p_kind , p.p_prop with
| PKCheck , _ -> ()
| PKSmoke , _ -> add_required hs "smoke-test"
| PKProp , IPAssigns {ias_kinstr=Kstmt _} ->
add_required hs "stmt-assigns"
| PKProp , IPAssigns {ias_kinstr=Kglobal} ->
add_required hs "fct-assigns"
| PKPropLoop , Property.IPAssigns _ -> add_required hs "loop-assigns"
| PKPropLoop , _ -> add_required hs "invariant"
| PKProp , _ -> add_required hs "property"
| PKTactic , _ -> add_required hs "tactic"
| PKEstablished , _ -> add_required hs "established"
| PKPreserved , _ -> add_required hs "preserved"
| PKVarDecr , _ -> add_required hs "decrease"
| PKVarPos , _ -> add_required hs "positive"
| PKVarRel , _ -> add_required hs "relation"
| PKAFctOut , _ -> add_required hs "return"
| PKAFctExit , _ -> add_required hs "exit"
| PKTerminates , _ -> add_required hs "terminates"
| PKDecreases , _ -> add_required hs "decreases"
| PKPre(kf,st,_) , _ ->
add_required hs ("precond-" ^ Kernel_function.get_name kf) ;
stmt_hints hs st
let rec term_hints hs t =
match t.term_node with
| TLval(lv,_) -> lval_hints hs lv
| TAddrOf(lv,_) -> lval_hints hs lv
| TCast (false, Ctype _,t) -> term_hints hs t
| TBinOp((PlusPI|MinusPI),a,_) -> term_hints hs a
| Tlet(_,t) -> term_hints hs t
| _ -> ()
and lval_hints hs = function
| TVar { lv_origin=Some { vorig_name=x } }
| TVar { lv_name=x } -> add_hint hs x
| TResult _ -> add_hint hs "result"
| TMem t -> add_hint hs "*" ; term_hints hs t
let assigns_hints hs froms =
List.iter (fun ({it_content=t},_) -> term_hints hs t) froms
let annot_hints hs = function
| AAssert(bs,ipred) | AInvariant(bs,_,ipred) ->
List.iter (add_hint hs) (ident_names ipred.tp_statement.pred_name) ;
List.iter (add_hint hs) bs
| AAssigns(bs,Writes froms) ->
List.iter (add_hint hs) bs ;
assigns_hints hs froms
| AAllocation _ | AAssigns(_,WritesAny) | AStmtSpec _
| AVariant _ | APragma _ | AExtended _ -> ()
let property_hints hs =
let open Property in function
| IPLemma {il_name; il_pred} ->
List.iter (add_required hs) (il_name::il_pred.tp_statement.pred_name)
| IPBehavior _ -> ()
| IPComplete {ic_bhvs} | IPDisjoint {ic_bhvs} ->
Datatype.String.Set.iter (add_required hs) ic_bhvs
| IPPredicate {ip_pred} ->
List.iter (add_hint hs) ip_pred.ip_content.tp_statement.pred_name
| IPExtended {ie_ext={ext_name}} -> List.iter (add_hint hs) [ext_name]
| IPCodeAnnot {ica_ca} -> annot_hints hs ica_ca.annot_content
| IPAssigns {ias_froms} -> assigns_hints hs ias_froms
| IPAllocation _
| IPFrom _ | Property.IPDecrease _ | Property.IPPropertyInstance _
| IPReachable _ | Property.IPAxiomatic _ | Property.IPOther _
| IPTypeInvariant _ | Property.IPGlobalInvariant _ -> ()
let prop_id_keys p =
begin
let hs = { hints=[] ; required=[] } in
let opt add f = function None -> () | Some x -> add hs (f x) in
propid_hints hs p ;
property_hints hs p.p_prop ;
opt add_required Kernel_function.get_name (Property.get_kf p.p_prop) ;
opt add_required
(fun b ->
if Cil.is_default_behavior b
then "default"
else b.b_name)
(Property.get_behavior p.p_prop) ;
opt add_hint (fun (k,_) -> Printf.sprintf "part-%d" k) p.p_part ;
kinstr_hints hs (Property.get_kinstr p.p_prop) ;
List.sort String.compare hs.required ,
List.sort String.compare hs.hints
end
let pp_goal_kind fmt = function
| PKTactic | PKSmoke | PKCheck
| PKProp | PKPropLoop | PKAFctOut | PKAFctExit | PKTerminates | PKDecreases
| PKPre _ -> ()
| PKEstablished -> Format.pp_print_string fmt "Establishment of "
| PKPreserved -> Format.pp_print_string fmt "Preservation of "
| PKVarDecr -> Format.pp_print_string fmt "Decreasing of "
| PKVarPos -> Format.pp_print_string fmt "Positivity of "
| PKVarRel -> Format.pp_print_string fmt "Follows relation "
let pp_goal_part fmt = function
| None -> ()
| Some(k,n) -> Format.fprintf fmt " (%d/%d)" (succ k) n
let pretty fmt pid =
begin
pp_goal_kind fmt pid.p_kind ;
Description.pp_property fmt pid.p_prop ;
pp_goal_part fmt pid.p_part ;
end
let pretty_context kf fmt pid =
begin
pp_goal_kind fmt pid.p_kind ;
Description.pp_localized ~kf ~ki:true ~kloc:true fmt pid.p_prop ;
pp_goal_part fmt pid.p_part ;
end
let is_check p = p.p_kind = PKCheck
let is_tactic p = p.p_kind = PKTactic
let is_smoke_test p = p.p_kind = PKSmoke
let is_assigns p =
match property_of_id p with
| Property.IPAssigns _ -> true
| _ -> false
let is_requires =
let open Property in function
| IPPredicate {ip_kind = PKRequires _} -> true
| _ -> false
let is_loop_preservation p =
match p.p_kind with
| PKPreserved ->
begin
match Property.get_kinstr p.p_prop with
| Kglobal -> Wp_parameters.fatal "Loop Preservation ? (%a)" Property.pretty p.p_prop
| Kstmt st -> Some st
end
| _ -> None
let user_prop_pid pid =
let p_prop = match pid.p_kind with
| PKPre (_,_,p_prop) -> p_prop
| _ -> property_of_id pid in
let names = user_prop_names p_prop in
let names = if is_smoke_test pid then "smoke" :: names else names in
match Property.get_kf p_prop with
| None -> names
| Some kf -> Kernel_function.get_name kf :: names
let select_default pid =
let names = user_prop_pid pid in
not (List.mem "no_wp" names)
let are_selected_names asked names =
if List.mem "no_wp" names then false
else
let is_minus s = try s.[0] = '-' with _ -> false in
let is_plus s = try s.[0] = '+' with _ -> false in
let remove_first s = String.sub s 1 ((String.length s) -1) in
let eval acc asked =
let is_minus,a = match acc with
| None -> if is_minus asked then true,true else false,false
| Some a -> (is_minus asked),a
in let eval () =
let asked = if is_minus || (is_plus asked)
then remove_first asked else asked
in List.mem asked names
in Some (if is_minus
then a && (not (eval ()))
else a || (eval ()))
in
match List.fold_left eval None asked with
| Some false -> false
| _ -> true
let select_by_name asked_names pid =
let names = user_prop_pid pid in
are_selected_names asked_names names
let select_for_behaviors bhvs pid =
let fors = Property.get_for_behaviors @@ property_of_id pid in
List.exists (fun b -> List.mem b fors) bhvs
let select_call_pre s_call asked_pre pid =
match pid.p_kind with
| PKPre (_, p_stmt, p_prop) ->
Stmt.equal s_call p_stmt &&
(match asked_pre with
| None -> true
| Some asked_pre -> Property.equal p_prop asked_pre)
| _ -> false
type a_kind = LoopAssigns | StmtAssigns
type assigns_desc = {
a_label : Clabels.c_label ;
a_stmt : Cil_types.stmt option ;
a_kind : a_kind ;
a_assigns : Cil_types.assigns ;
}
let mk_asm_assigns_desc s = {
a_label = Clabels.stmt s ;
a_stmt = Some s ;
a_kind = StmtAssigns ;
a_assigns = WritesAny ;
}
let mk_loop_assigns_desc s assigns = {
a_label = Clabels.stmt s ;
a_stmt = Some s ;
a_kind = LoopAssigns ;
a_assigns = Writes assigns
}
let mk_stmt_assigns_desc s assigns = {
a_label = Clabels.stmt s ;
a_stmt = Some s ;
a_kind = StmtAssigns ;
a_assigns = Writes assigns ;
}
let mk_stmt_assigns_any_desc s = {
a_label = Clabels.stmt s ;
a_stmt = Some s ;
a_kind = StmtAssigns ;
a_assigns = WritesAny ;
}
let mk_init_assigns = {
a_label = Clabels.init ;
a_stmt = None ;
a_kind = StmtAssigns ;
a_assigns = WritesAny ;
}
let mk_kf_assigns_desc assigns = {
a_label = Clabels.pre ;
a_stmt = None ;
a_kind = StmtAssigns ;
a_assigns = Writes assigns ;
}
let is_call_assigns = function
| {a_stmt=Some {skind=Instr(Call _ | Local_init (_, ConsInit _, _)) } }
-> true
| _ -> false
let pp_assigns_desc fmt a = Wp_error.pp_assigns fmt a.a_assigns
(**
* 2 kinds of annotations can be found : predicates and assigns.
* because assigns properties can only be translated into predicates
* by the memory model.
* - Assigns properties are composed of the assigns list from Cil,
* and a label to know where to stop.
* - Predicates are just the predicate type from Cil.
*)
type pred_info = prop_id * Cil_types.predicate
type variant_info = prop_id * Cil_types.variant
let mk_pred_info id p = (id, p)
let pred_info_id (id, _) = id
let pp_pred_of_pred_info fmt (_id, p) = Printer.pp_predicate fmt p
let pp_pred_info fmt (id, p) =
Format.fprintf fmt "(@[%a:@ %a@])" pp_propid id Printer.pp_predicate p
type assigns_info = prop_id * assigns_desc
let assigns_info_id (id,_) = id
type assigns_full_info =
AssignsLocations of assigns_info
| AssignsAny of assigns_desc
| NoAssignsInfo
let empty_assigns_info = NoAssignsInfo
let mk_assigns_info id a = AssignsLocations (id, a)
let mk_stmt_any_assigns_info s =
let a = {
a_label = Clabels.stmt s ;
a_stmt = Some s ;
a_kind = StmtAssigns ;
a_assigns = WritesAny ;
} in
AssignsAny a
let mk_kf_any_assigns_info () =
let a = {
a_label = Clabels.pre ;
a_stmt = None ;
a_kind = StmtAssigns ;
a_assigns = WritesAny ;
} in
AssignsAny a
let mk_loop_any_assigns_info s =
let a = {
a_label = Clabels.stmt s ;
a_stmt = Some s ;
a_kind = LoopAssigns ;
a_assigns = WritesAny ;
} in
AssignsAny a
let pp_assign_info k fmt a = match a with
| NoAssignsInfo -> ()
| AssignsAny a ->
let pkind =
match a.a_kind with
| StmtAssigns -> ""
| LoopAssigns -> "loop"
in
Format.fprintf fmt "%s(@@%a): %s assigns everything@."
k Clabels.pretty a.a_label pkind
| AssignsLocations (_,a) ->
Format.fprintf fmt "%s(@@%a): %a@." k
Clabels.pretty a.a_label
pp_assigns_desc a
let merge_assign_info a1 a2 = match a1,a2 with
| NoAssignsInfo, a | a, NoAssignsInfo -> a
| (AssignsLocations _ | AssignsAny _),
(AssignsLocations _ | AssignsAny _) ->
Wp_parameters.fatal "Several assigns ?"
type axiom_info = prop_id * LogicUsage.logic_lemma
let mk_axiom_info lemma =
let id = mk_lemma_id lemma in (id, lemma)
let pp_axiom_info fmt (id,thm) =
Format.fprintf fmt "(@[%a:@ %a@])" pp_propid id
Printer.pp_predicate thm.LogicUsage.lem_predicate.tp_statement
let split_bag job pid goals =
let n = Bag.length goals in
if n <= 1 then Bag.iter (job pid) goals else
let k = ref 0 in
Bag.iter
(fun g ->
let pid_k = mk_part pid (!k,n) in
incr k ; job pid_k g)
goals
let split_map f pid gs =
let n = List.length gs in
if n <= 1 then List.map (f pid) gs else
let k = ref 0 in
List.map (fun g ->
let pid_k = mk_part pid (!k,n) in
incr k ; f pid_k g
) gs
(** About proofs *)
let subproofs id = match id.p_kind with
| PKCheck -> 0
| PKProp | PKSmoke | PKTactic | PKPre _ | PKPropLoop
| PKTerminates | PKDecreases | PKVarRel -> 1
| PKEstablished | PKPreserved
| PKVarDecr | PKVarPos
| PKAFctExit | PKAFctOut -> 2
let subproof_idx id = match id.p_kind with
| PKCheck -> (-1)
| PKProp | PKTactic | PKPre _ | PKSmoke | PKPropLoop
| PKTerminates | PKDecreases | PKVarRel -> 0
| PKPreserved -> 0
| PKEstablished-> 1
| PKVarDecr -> 0
| PKVarPos -> 1
| PKAFctOut -> 0
| PKAFctExit -> 1
(** find the outer loop in which the stmt is. *)
let get_loop_stmt kf stmt =
let rec is_in_blk b = List.exists is_in_stmt b.bstmts
and is_in_stmt s = if s.sid = stmt.sid then true
else match s.skind with
| If (_, b1, b2,_) -> is_in_blk b1 || is_in_blk b2
| Switch (_, b, _, _) | Block b -> is_in_blk b
| UnspecifiedSequence seq ->
let b = Cil.block_from_unspecified_sequence seq in
is_in_blk b
| Loop (_, b, _, _, _) -> is_in_blk b
| _ -> false
and find_loop_in_blk blk = find_loop_in_stmts blk.bstmts
and find_loop_in_stmts l = match l with
| [] -> None
| s::tl ->
(match find_loop_in_stmt s with Some l -> Some l
| None -> find_loop_in_stmts tl)
and find_loop_in_stmt s = match s.skind with
| (Loop _) -> if is_in_stmt s then Some s else None
| If (_, b1, b2,_) ->
(match find_loop_in_blk b1 with Some l -> Some l
| None -> find_loop_in_blk b2)
| Switch (_, b, _, _) | Block b -> find_loop_in_blk b
| UnspecifiedSequence seq ->
let b = Cil.block_from_unspecified_sequence seq in
find_loop_in_blk b
| _ -> None
in let f = Kernel_function.get_definition kf in
find_loop_in_blk f.sbody
(** Quite don't understand what is going on here... what is it supposed to do ?
* [2011-07-07-Anne] *)
let get_induction p =
let get_stmt = let open Property in function
| IPDecrease {id_kf;id_kinstr=Kstmt stmt} -> Some (id_kf, stmt)
| IPCodeAnnot {ica_kf;ica_stmt} -> Some (ica_kf, ica_stmt)
| IPAssigns {ias_kf; ias_kinstr=Kstmt stmt} -> Some (ias_kf, stmt)
| _ -> None
in match p.p_kind with
| PKCheck | PKSmoke | PKAFctOut | PKAFctExit | PKPre _
| PKTactic | PKTerminates | PKDecreases ->
None
| PKProp ->
let loop_stmt_opt = match get_stmt (property_of_id p) with
| None -> None
| Some (kf, s) -> get_loop_stmt kf s
in loop_stmt_opt
| PKPropLoop ->
let open Property in
let loop_stmt_opt = match property_of_id p with
| IPCodeAnnot {ica_kf; ica_stmt;
ica_ca = {annot_content = AInvariant(_, loop, _)}} ->
if loop then Some ica_stmt
else get_loop_stmt ica_kf ica_stmt
| IPAssigns {ias_kinstr=Kstmt stmt; ias_bhv = Id_loop _} ->
Some stmt
| _ -> None
in loop_stmt_opt
| PKEstablished|PKVarDecr|PKVarPos|PKVarRel|PKPreserved ->
(match get_stmt (property_of_id p) with
| None -> None | Some (_, s) -> Some s)
let filter_status pid =
Wp_parameters.StatusAll.get () ||
begin
let module C = Property_status.Consolidation in
match C.get (property_of_id pid) with
| C.Never_tried -> true
| C.Considered_valid | C.Inconsistent _ -> false
| C.Valid _ | C.Valid_under_hyp _
| C.Invalid_but_dead _ | C.Valid_but_dead _ | C.Unknown_but_dead _ ->
Wp_parameters.StatusTrue.get ()
| C.Unknown _ -> Wp_parameters.StatusMaybe.get ()
| C.Invalid _ | C.Invalid_under_hyp _ -> Wp_parameters.StatusFalse.get ()
end
type proof = {
target : Property.t ;
proved : proofpart array ;
mutable invalid : bool ;
mutable dependencies : Property.Set.t ;
} and proofpart =
| Noproof
| Complete
| Parts of Bitvector.t
let target p = p.target
let dependencies p =
Property.Set.elements (Property.Set.remove p.target p.dependencies)
let create_proof ip =
let n = subproofs ip in
{
target = property_of_id ip ;
proved = Array.make n Noproof ;
dependencies = Property.Set.empty ;
invalid = false ;
}
let add_proof pf ip hs =
begin
if not (Property.equal (property_of_id ip) pf.target)
then Wp_parameters.fatal "Partial proof inconsistency" ;
List.iter
(fun iph ->
if not (is_requires iph) then
pf.dependencies <- Property.Set.add iph pf.dependencies
) hs ;
let k = subproof_idx ip in
match parts_of_id ip with
| None -> pf.proved.(k) <- Complete
| Some(p,n) ->
match pf.proved.(k) with
| Complete -> ()
| Noproof ->
let bv = Bitvector.create n in
Bitvector.set_range bv 0 (p-1) ;
Bitvector.set_range bv (p+1) (n-1) ;
pf.proved.(k) <- Parts bv
| Parts bv ->
Bitvector.clear bv p ;
if Bitvector.is_empty bv
then pf.proved.(k) <- Complete
end
let add_invalid_proof pf = pf.invalid <- true
let is_composed pf =
Array.length pf.proved > 1
let is_proved pf =
Array.for_all (function Complete -> true | _ -> false) pf.proved
let is_invalid pf =
pf.invalid && not (is_proved pf)