From 0c70644129abf36067add678b5b5fe2f5cc0cda0 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Mon, 7 Sep 2020 15:37:12 +0200
Subject: [PATCH] [kernel] Update Property to use a Set for the complete and
disjoint behaviors
---
src/kernel_services/ast_data/property.ml | 30 ++++++++++++-------
src/kernel_services/ast_data/property.mli | 2 +-
.../ast_printing/description.ml | 19 ++++++++----
.../wp/tests/wp/oracle/wp_behav.res.oracle | 2 +-
.../tests/wp/oracle/wp_behavior.0.res.oracle | 4 +--
.../tests/wp/oracle/wp_behavior.1.res.oracle | 4 +--
.../wp/oracle_qualif/wp_behav.0.res.oracle | 2 +-
.../oracle/frama_c_hashtbl_solved.res.oracle | 8 ++---
.../frama_c_hashtbl_solved.res.oracle | 8 ++---
src/plugins/wp/wpPropId.ml | 9 ++++--
10 files changed, 53 insertions(+), 35 deletions(-)
diff --git a/src/kernel_services/ast_data/property.ml b/src/kernel_services/ast_data/property.ml
index 4029b382948..76dbce8cdaf 100644
--- a/src/kernel_services/ast_data/property.ml
+++ b/src/kernel_services/ast_data/property.ml
@@ -76,7 +76,7 @@ type identified_complete = {
ic_kf : kernel_function;
ic_kinstr : kinstr;
ic_active : Datatype.String.Set.t;
- ic_bhvs : string list
+ ic_bhvs : Datatype.String.Set.t
}
type identified_disjoint = identified_complete
@@ -461,14 +461,16 @@ include Datatype.Make_with_collections
| IPCodeAnnot {ica_ca} -> Cil_printer.pp_code_annotation fmt ica_ca
| IPComplete {ic_active; ic_bhvs} ->
Format.fprintf fmt "complete@ %a"
- (Pretty_utils.pp_list ~sep:","
- (fun fmt s -> Format.fprintf fmt "@ %s" s))
+ (Pretty_utils.pp_iter ~sep:","
+ Datatype.String.Set.iter
+ (fun fmt s -> Format.fprintf fmt "@ %s" s))
ic_bhvs;
pp_active fmt ic_active
| IPDisjoint {ic_active; ic_bhvs} ->
Format.fprintf fmt "disjoint@ %a"
- (Pretty_utils.pp_list ~sep:","
- (fun fmt s -> Format.fprintf fmt "@ %s" s))
+ (Pretty_utils.pp_iter ~sep:","
+ Datatype.String.Set.iter
+ (fun fmt s -> Format.fprintf fmt "@ %s" s))
ic_bhvs;
pp_active fmt ic_active
| IPAllocation {ial_allocs=(f,a)} ->
@@ -511,11 +513,11 @@ include Datatype.Make_with_collections
(* complete list is more likely to discriminate than active list. *)
Hashtbl.hash
(6, Kf.hash f, Kinstr.hash ki,
- (y:string list), (x:Datatype.String.Set.t))
+ Datatype.String.Set.hash y, Datatype.String.Set.hash x)
| IPDisjoint {ic_kf=f; ic_kinstr=ki; ic_bhvs=y; ic_active=x} ->
Hashtbl.hash
(7, Kf.hash f, Kinstr.hash ki,
- (y: string list), (x:Datatype.String.Set.t))
+ Datatype.String.Set.hash y, Datatype.String.Set.hash x)
| IPAssigns {ias_kf=f; ias_kinstr=ki; ias_bhv=b} ->
Hashtbl.hash (8, Kf.hash f, Kinstr.hash ki, hash_bhv_loop b)
| IPFrom {if_kf=kf; if_kinstr=ki; if_bhv=b; if_from=(t, _)} ->
@@ -572,7 +574,7 @@ include Datatype.Make_with_collections
IPComplete {ic_kf=f2;ic_kinstr=ki2;ic_active=a2;ic_bhvs=x2}
| IPDisjoint {ic_kf=f1;ic_kinstr=ki1;ic_active=a1;ic_bhvs=x1},
IPDisjoint {ic_kf=f2;ic_kinstr=ki2;ic_active=a2;ic_bhvs=x2} ->
- Kf.equal f1 f2 && Kinstr.equal ki1 ki2 && a1 = a2 && x1 = x2
+ Kf.equal f1 f2 && Kinstr.equal ki1 ki2 && a1 = a2 && Datatype.String.Set.equal x1 x2
| IPAllocation {ial_kf=f1;ial_kinstr=ki1;ial_bhv=b1},
IPAllocation {ial_kf=f2;ial_kinstr=ki2;ial_bhv=b2}
| IPAssigns {ias_kf=f1;ias_kinstr=ki1;ias_bhv=b1},
@@ -641,7 +643,7 @@ include Datatype.Make_with_collections
if n = 0 then
let n = Kinstr.compare ki1 ki2 in
if n = 0 then
- let n = Extlib.compare_basic x1 x2 in
+ let n = Datatype.String.Set.compare x1 x2 in
if n = 0 then
Datatype.String.Set.compare a1 a2
else n
@@ -824,13 +826,13 @@ let rec pretty_debug fmt = function
Cil_types_debug.pp_kernel_function ic_kf
Cil_types_debug.pp_kinstr ic_kinstr
Datatype.String.Set.pretty ic_active
- (Cil_types_debug.pp_list Cil_types_debug.pp_string) ic_bhvs
+ Datatype.String.Set.pretty ic_bhvs
| IPDisjoint {ic_kf; ic_kinstr; ic_active; ic_bhvs} ->
Format.fprintf fmt "IPDisjoint(%a,%a,%a,%a)"
Cil_types_debug.pp_kernel_function ic_kf
Cil_types_debug.pp_kinstr ic_kinstr
Datatype.String.Set.pretty ic_active
- (Cil_types_debug.pp_list Cil_types_debug.pp_string) ic_bhvs
+ Datatype.String.Set.pretty ic_bhvs
| IPDecrease {id_kf; id_kinstr; id_ca; id_variant} ->
Format.fprintf fmt "IPDecrease(%a,%a,%a,%a)"
Cil_types_debug.pp_kernel_function id_kf
@@ -1023,9 +1025,11 @@ struct
| AExtended(_,_,{ext_name}) -> ext_name
in Format.asprintf "%s%s%a" (kf_prefix kf) name pp_code_annot_names ca
| IPComplete {ic_kf=kf; ic_kinstr=ki; ic_active=a; ic_bhvs=lb} ->
+ let lb = Datatype.String.Set.elements lb in
Format.asprintf "%s%s%acomplete%a"
(kf_prefix kf) (ki_prefix ki) active_prefix a pp_names lb
| IPDisjoint {ic_kf=kf; ic_kinstr=ki; ic_active=a; ic_bhvs=lb} ->
+ let lb = Datatype.String.Set.elements lb in
Format.asprintf "%s%s%adisjoint%a"
(kf_prefix kf) (ki_prefix ki) active_prefix a pp_names lb
| IPDecrease {id_kf=kf; id_ca=None; id_variant=variant} ->
@@ -1235,8 +1239,10 @@ struct
[K kf ; A "loop_allocates" ]
| IPComplete {ic_kf=kf; ic_bhvs=cs} ->
+ let cs = Datatype.String.Set.elements cs in
(K kf :: A "complete" :: List.map (fun a -> A a) cs)
| IPDisjoint {ic_kf=kf; ic_bhvs=cs} ->
+ let cs = Datatype.String.Set.elements cs in
(K kf :: A "disjoint" :: List.map (fun a -> A a) cs)
| IPReachable {ir_kf=None} -> []
@@ -1449,6 +1455,7 @@ let ip_all_of_behavior kf st ~active b =
@ List.map (ip_of_extended (e_loc_of_stmt kf st)) b.b_extended
let ip_of_complete ic_kf ic_kinstr ~active ic_bhvs =
+ let ic_bhvs = Datatype.String.Set.of_list ic_bhvs in
let ic_active = Datatype.String.Set.of_list active in
IPComplete {ic_kf; ic_kinstr; ic_active; ic_bhvs}
@@ -1456,6 +1463,7 @@ let ip_complete_of_spec kf st ~active s =
List.map (ip_of_complete kf st ~active) s.spec_complete_behaviors
let ip_of_disjoint ic_kf ic_kinstr ~active ic_bhvs =
+ let ic_bhvs = Datatype.String.Set.of_list ic_bhvs in
let ic_active = Datatype.String.Set.of_list active in
IPDisjoint {ic_kf; ic_kinstr; ic_active; ic_bhvs}
diff --git a/src/kernel_services/ast_data/property.mli b/src/kernel_services/ast_data/property.mli
index 395250cf2e3..ef1f193333d 100644
--- a/src/kernel_services/ast_data/property.mli
+++ b/src/kernel_services/ast_data/property.mli
@@ -100,7 +100,7 @@ type identified_complete = {
ic_kf : kernel_function;
ic_kinstr : kinstr;
ic_active : Datatype.String.Set.t;
- ic_bhvs : string list
+ ic_bhvs : Datatype.String.Set.t
}
(** Same as for {!identified_behavior}. *)
diff --git a/src/kernel_services/ast_printing/description.ml b/src/kernel_services/ast_printing/description.ml
index e9de181388e..8ccda1048a0 100644
--- a/src/kernel_services/ast_printing/description.ml
+++ b/src/kernel_services/ast_printing/description.ml
@@ -95,12 +95,17 @@ let pp_bhv fmt bhv =
if not (Cil.is_default_behavior bhv) then
Format.fprintf fmt " for '%s'" bhv.b_name
-let pp_bhvs fmt = function
- | [] -> ()
- | b::bs ->
- Format.fprintf fmt " @[<hov 0>'%s'" b ;
- List.iter (fun b -> Format.fprintf fmt ",@ '%s'" b) bs ;
- Format.fprintf fmt "@]"
+let pp_bhvs fmt bhvs =
+ if Datatype.String.Set.is_empty bhvs then
+ ()
+ else
+ Pretty_utils.pp_iter
+ ~pre:" @[<hov 0>"
+ ~suf:"@]"
+ ~sep:",@ "
+ Datatype.String.Set.iter
+ (fun fmt s -> Format.fprintf fmt "'%s'" s)
+ fmt bhvs
let pp_for fmt = function
| [] -> ()
@@ -492,8 +497,10 @@ let rec ip_order = function
| IPBehavior {ib_kf;ib_kinstr;ib_active;ib_bhv} ->
[I 6;F ib_kf;K ib_kinstr;B ib_bhv; A ib_active]
| IPComplete {ic_kf;ic_kinstr;ic_active;ic_bhvs} ->
+ let ic_bhvs = Datatype.String.Set.elements ic_bhvs in
[I 7;F ic_kf;K ic_kinstr; A ic_active] @ for_order 0 ic_bhvs
| IPDisjoint {ic_kf;ic_kinstr;ic_active;ic_bhvs} ->
+ let ic_bhvs = Datatype.String.Set.elements ic_bhvs in
[I 8;F ic_kf;K ic_kinstr; A ic_active] @ for_order 0 ic_bhvs
| IPPredicate {ip_kind;ip_kf;ip_kinstr} ->
[I 9;F ip_kf;K ip_kinstr] @ kind_order ip_kind
diff --git a/src/plugins/wp/tests/wp/oracle/wp_behav.res.oracle b/src/plugins/wp/tests/wp/oracle/wp_behav.res.oracle
index 5d027100e99..1482e87b434 100644
--- a/src/plugins/wp/tests/wp/oracle/wp_behav.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle/wp_behav.res.oracle
@@ -30,7 +30,7 @@ Prove: true.
Function bhv
------------------------------------------------------------
-Goal Complete behaviors 'pos', 'neg':
+Goal Complete behaviors 'neg', 'pos':
Assume { Type: is_sint32(n). (* Pre-condition *) Have: n != 0. }
Prove: (0 < n) \/ (n < 0).
diff --git a/src/plugins/wp/tests/wp/oracle/wp_behavior.0.res.oracle b/src/plugins/wp/tests/wp/oracle/wp_behavior.0.res.oracle
index c28768d2976..c377eb93bf7 100644
--- a/src/plugins/wp/tests/wp/oracle/wp_behavior.0.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle/wp_behavior.0.res.oracle
@@ -6,7 +6,7 @@
Function behaviors
------------------------------------------------------------
-Goal Complete behaviors 'Y', 'X':
+Goal Complete behaviors 'X', 'Y':
Assume {
(* Pre-condition *)
Have: P_R.
@@ -19,7 +19,7 @@ Prove: P_CX \/ P_CY.
------------------------------------------------------------
-Goal Disjoint behaviors 'Y', 'X':
+Goal Disjoint behaviors 'X', 'Y':
Assume {
(* Pre-condition *)
Have: P_R.
diff --git a/src/plugins/wp/tests/wp/oracle/wp_behavior.1.res.oracle b/src/plugins/wp/tests/wp/oracle/wp_behavior.1.res.oracle
index e6e7eac38d3..8d98a45587a 100644
--- a/src/plugins/wp/tests/wp/oracle/wp_behavior.1.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle/wp_behavior.1.res.oracle
@@ -6,13 +6,13 @@
Function behaviors
------------------------------------------------------------
-Goal Complete behaviors 'Y', 'X':
+Goal Complete behaviors 'X', 'Y':
Assume { (* Pre-condition *) Have: P_R. }
Prove: P_CX \/ P_CY.
------------------------------------------------------------
-Goal Disjoint behaviors 'Y', 'X':
+Goal Disjoint behaviors 'X', 'Y':
Assume { (* Pre-condition *) Have: P_R. }
Prove: (!P_CX) \/ (!P_CY).
diff --git a/src/plugins/wp/tests/wp/oracle_qualif/wp_behav.0.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/wp_behav.0.res.oracle
index 36780873763..faa679c9669 100644
--- a/src/plugins/wp/tests/wp/oracle_qualif/wp_behav.0.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle_qualif/wp_behav.0.res.oracle
@@ -22,7 +22,7 @@
[wp] [Qed] Goal typed_min_disjoint_bx_by : Valid
[wp] [Qed] Goal typed_min_bx_ensures_qed_ok : Valid
[wp] [Qed] Goal typed_min_by_ensures_qed_ok : Valid
-[wp] [Alt-Ergo] Goal typed_bhv_complete_pos_neg : Valid
+[wp] [Alt-Ergo] Goal typed_bhv_complete_neg_pos : Valid
[wp] [Qed] Goal typed_bhv_pos_ensures_qed_ok : Valid
[wp] [Qed] Goal typed_bhv_neg_ensures_qed_ok : Valid
[wp] [Qed] Goal typed_stmt_contract_requires_qed_ok : Valid
diff --git a/src/plugins/wp/tests/wp_gallery/oracle/frama_c_hashtbl_solved.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle/frama_c_hashtbl_solved.res.oracle
index b4db2ed7bdd..2429963d412 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle/frama_c_hashtbl_solved.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle/frama_c_hashtbl_solved.res.oracle
@@ -7,8 +7,8 @@
[rte] annotating function init
[rte] annotating function mem_binding
[rte] annotating function size
-[wp] Goal typed_eq_string_complete_not_eq_eq : trivial
-[wp] Goal typed_eq_string_disjoint_not_eq_eq : trivial
+[wp] Goal typed_eq_string_complete_eq_not_eq : trivial
+[wp] Goal typed_eq_string_disjoint_eq_not_eq : trivial
[wp] Goal typed_eq_string_loop_invariant_preserved : not tried
[wp] Goal typed_eq_string_loop_invariant_established : not tried
[wp] Goal typed_eq_string_loop_invariant_2_preserved : not tried
@@ -111,8 +111,8 @@
[wp] Goal typed_add_full_assigns_normal_part7 : not tried
[wp] Goal typed_add_full_assigns_normal_part8 : not tried
[wp] Goal typed_add_full_assigns_normal_part9 : not tried
-[wp] Goal typed_mem_binding_complete_not_found_found : not tried
-[wp] Goal typed_mem_binding_disjoint_not_found_found : not tried
+[wp] Goal typed_mem_binding_complete_found_not_found : not tried
+[wp] Goal typed_mem_binding_disjoint_found_not_found : not tried
[wp] Goal typed_mem_binding_loop_invariant_preserved : not tried
[wp] Goal typed_mem_binding_loop_invariant_established : not tried
[wp] Goal typed_mem_binding_loop_invariant_2_preserved : not tried
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.res.oracle
index aa0a56a75fb..b9066d9921a 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.res.oracle
@@ -3,8 +3,8 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 102 goals scheduled
-[wp] [Qed] Goal typed_eq_string_complete_not_eq_eq : Valid
-[wp] [Qed] Goal typed_eq_string_disjoint_not_eq_eq : Valid
+[wp] [Qed] Goal typed_eq_string_complete_eq_not_eq : Valid
+[wp] [Qed] Goal typed_eq_string_disjoint_eq_not_eq : Valid
[wp] [Alt-Ergo] Goal typed_eq_string_loop_invariant_preserved : Valid
[wp] [Qed] Goal typed_eq_string_loop_invariant_established : Valid
[wp] [Alt-Ergo] Goal typed_eq_string_loop_invariant_2_preserved : Valid
@@ -79,8 +79,8 @@
[wp] [Alt-Ergo] Goal typed_add_full_assigns_normal_part7 : Valid
[wp] [Alt-Ergo] Goal typed_add_full_assigns_normal_part8 : Valid
[wp] [Qed] Goal typed_add_full_assigns_normal_part9 : Valid
-[wp] [Alt-Ergo] Goal typed_mem_binding_complete_not_found_found : Valid
-[wp] [Alt-Ergo] Goal typed_mem_binding_disjoint_not_found_found : Valid
+[wp] [Alt-Ergo] Goal typed_mem_binding_complete_found_not_found : Valid
+[wp] [Alt-Ergo] Goal typed_mem_binding_disjoint_found_not_found : Valid
[wp] [Alt-Ergo] Goal typed_mem_binding_loop_invariant_preserved : Valid
[wp] [Alt-Ergo] Goal typed_mem_binding_loop_invariant_established : Valid
[wp] [Alt-Ergo] Goal typed_mem_binding_loop_invariant_2_preserved : Valid
diff --git a/src/plugins/wp/wpPropId.ml b/src/plugins/wp/wpPropId.ml
index 22988574935..441d8cbfb9a 100644
--- a/src/plugins/wp/wpPropId.ml
+++ b/src/plugins/wp/wpPropId.ml
@@ -458,8 +458,11 @@ let get_propid = Names.get_prop_id_name
let pp_propid fmt pid =
Format.pp_print_string fmt (get_propid pid)
-let pp_names fmt l = match l with [] -> () | _ ->
- Format.fprintf fmt "_%a" (Wp_error.pp_string_list ~empty:"" ~sep:"_") l
+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
@@ -670,7 +673,7 @@ let property_hints hs =
List.iter (add_required hs) (il_name::il_pred.tp_statement.pred_name)
| IPBehavior _ -> ()
| IPComplete {ic_bhvs} | IPDisjoint {ic_bhvs} ->
- List.iter (add_required hs) 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]
--
GitLab