Merge branch 'feature/stable/wp-fix-file-output-naming' into 'stable/potassium'

[WP] factorize uniqueness handling of properties id

See merge request frama-c/frama-c!2284

src/plugins/wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle

@@ -13,7 +13,7 @@
 [wp] [Qed] Goal typed_call_main_ensures_qed_ok : Valid
 [wp] [Qed] Goal typed_call_main_call_main_requires_qed_ok_Rmain : Valid
 [wp] [Qed] Goal typed_double_call_call_f_requires_qed_ok_Rf : Valid
-[wp] [Alt-Ergo] Goal typed_double_call_call_f_requires_qed_ok_Rf : Valid
+[wp] [Alt-Ergo] Goal typed_double_call_call_f_2_requires_qed_ok_Rf : Valid
 [wp] [Qed] Goal typed_main_requires_qed_ok_Rmain : Valid
 [wp] [Qed] Goal typed_main_ensures_qed_ok_Emain : Valid
 [wp] [Qed] Goal typed_main_call_f_requires_qed_ok_Rf : Valid

src/plugins/wp/tests/wp_bts/oracle_qualif/nupw-bcl-bts1120.res.oracle

@@ -17,7 +17,7 @@
 [wp] [Qed] Goal typed_g_assigns_normal_part2 : Valid
 [wp] [Qed] Goal typed_g_assigns_normal_part3 : Valid
 [wp] [Qed] Goal typed_unreachable_smt_with_contract_ensures_ok_2 : Valid
-[wp] [Qed] Goal typed_unreachable_smt_with_contract_call_f_with_precond_requires_ok : Valid
+[wp] [Qed] Goal typed_unreachable_smt_with_contract_call_f_with_precond_2_requires_ok : Valid
 [wp] Proved goals:    8 / 8
   Qed:             8
 [wp] Report in:  'tests/wp_bts/oracle_qualif/nupw-bcl-bts1120.0.report.json'

src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var.res.oracle

@@ -65,7 +65,7 @@
 [wp] [Qed] Goal typed_ref_call_ref_valid_assigns_normal_part4 : Valid
 [wp] [Qed] Goal typed_ref_call_ref_valid_assigns_normal_part5 : Valid
 [wp] [Qed] Goal typed_ref_call_ref_valid_call_ref_valid_requires : Valid
-[wp] [Qed] Goal typed_ref_call_ref_valid_call_ref_valid_requires : Valid
+[wp] [Qed] Goal typed_ref_call_ref_valid_call_ref_valid_2_requires : Valid
 [wp] [Qed] Goal typed_ref_call_two_ref_ensures : Valid
 [wp] [Qed] Goal typed_ref_call_two_ref_assigns_exit_part1 : Valid
 [wp] [Qed] Goal typed_ref_call_two_ref_assigns_exit_part2 : Valid

src/plugins/wp/tests/wp_plugin/oracle_qualif/injector.0.res.oracle

@@ -5,7 +5,7 @@
 [wp] Warning: Missing RTE guards
 [wp] 13 goals scheduled
 [wp] [Qed] Goal typed_f_call_g_requires : Valid
-[wp] [Qed] Goal typed_f_call_g_requires : Valid
+[wp] [Qed] Goal typed_f_call_g_2_requires : Valid
 [wp] [Qed] Goal typed_f_FST_FAIL_ensures_qed_ok : Valid
 [wp] [Qed] Goal typed_f_FST_FAIL_ensures_qed_ok_2 : Valid
 [wp] [Qed] Goal typed_f_FST_FAIL_ensures_qed_ok_3 : Valid

src/plugins/wp/tests/wp_typed/oracle_qualif/user_collect.res.oracle

@@ -8,19 +8,19 @@
 [wp] [Alt-Ergo] Goal typed_caller_ensures_P1 : Valid
 [wp] [Alt-Ergo] Goal typed_caller_ensures_P2 : Valid
 [wp] [Alt-Ergo] Goal typed_caller_call_job_requires : Valid
-[wp] [Alt-Ergo] Goal typed_caller_call_job_requires : Valid
+[wp] [Alt-Ergo] Goal typed_caller_call_job_2_requires : Valid
 [wp] [Qed] Goal typed_caller2_ensures_K : Valid
 [wp] [Alt-Ergo] Goal typed_caller2_ensures_Q1 : Valid
 [wp] [Alt-Ergo] Goal typed_caller2_ensures_Q2 : Valid
 [wp] [Alt-Ergo] Goal typed_caller2_ensures_R : Valid
 [wp] [Alt-Ergo] Goal typed_caller2_call_job2_requires : Valid
-[wp] [Alt-Ergo] Goal typed_caller2_call_job2_requires : Valid
+[wp] [Alt-Ergo] Goal typed_caller2_call_job2_2_requires : Valid
 [wp] [Qed] Goal typed_caller3_ensures_K : Valid
 [wp] [Alt-Ergo] Goal typed_caller3_ensures_Q1 : Valid
 [wp] [Alt-Ergo] Goal typed_caller3_ensures_Q2 : Valid
 [wp] [Alt-Ergo] Goal typed_caller3_ensures_R : Valid
 [wp] [Alt-Ergo] Goal typed_caller3_call_job3_requires : Valid
-[wp] [Alt-Ergo] Goal typed_caller3_call_job3_requires : Valid
+[wp] [Alt-Ergo] Goal typed_caller3_call_job3_2_requires : Valid
 [wp] [Qed] Goal typed_job_ensures_K : Valid
 [wp] [Qed] Goal typed_job_ensures_P : Valid
 [wp] [Qed] Goal typed_job_assigns_part1 : Valid

src/plugins/wp/wpPropId.ml

@@ -232,22 +232,27 @@ module PropId =
 (* --- Lagacy Naming                                                      --- *)
 (* -------------------------------------------------------------------------- *)
 
-module LegacyNames :
+module NameUniquify(D:Datatype.S_with_collections)(S:sig
+    val name: string
+    val basename: D.t -> string
+  end) :
 sig
-  val get_prop_id_name: prop_id -> string
-end = struct
+  val unique_basename: D.t -> string
+end
+=
+struct
 
   module NamesTbl = State_builder.Hashtbl(Datatype.String.Hashtbl)(Datatype.Int)
       (struct
-        let name = "WpPropertyNames"
+        let name = S.name^"Names"
         let dependencies = [ ]
         let size = 97
       end)
 
   module IndexTbl =
-    State_builder.Hashtbl(PropId.Hashtbl)(Datatype.String)
+    State_builder.Hashtbl(D.Hashtbl)(Datatype.String)
       (struct
-        let name = "WpPropertyIndex"
+        let name = S.name^"Index"
         let dependencies =
           [ Ast.self;
             NamesTbl.self;
@@ -258,6 +263,38 @@ end = struct
         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
+      (* this basename is already reserved *)
+      let n,unique_name = Extlib.make_unique_name NamesTbl.mem ~sep:"_" ~start:speed_up_start basename
+      in NamesTbl.replace basename (succ n) ; (* to speed up Extlib.make_unique_name for next time *)
+      unique_name
+    with Not_found -> (* first time that basename is reserved *)
+      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 -> (* first time we are asking for a name for that [ip] *)
+      let unique_name = reserve_name_id pid in
+      IndexTbl.add pid unique_name ;
+      unique_name
+
+end
+
+module LegacyNames :
+sig
+  val get_prop_id_name: prop_id -> string
+end = struct
+
   let base_id_prop_txt = Property.LegacyNames.get_prop_name_id
 
   let basename_of_prop_id p =
@@ -296,29 +333,17 @@ end = struct
             Printf.sprintf "%s_part%06d" basename (succ k)
     in normalize_basename basename
 
-  (** 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 = get_prop_id_basename pid in
-    try
-      let speed_up_start = NamesTbl.find basename in
-      (* this basename is already reserved *)
-      let n,unique_name = Extlib.make_unique_name NamesTbl.mem ~sep:"_" ~start:speed_up_start basename
-      in NamesTbl.replace basename (succ n) ; (* to speed up Extlib.make_unique_name for next time *)
-      unique_name
-    with Not_found -> (* first time that basename is reserved *)
-      NamesTbl.add basename 2 ;
-      basename
+
+  module UniquifyPropId = NameUniquify(PropId)(struct
+      let name = "WpProperty"
+      let basename = get_prop_id_basename
+    end)
+
 
   (** returns a unique name identifying the property.
       This name is built from the basename of the property. *)
   let get_prop_id_name pid =
-    try IndexTbl.find pid
-    with Not_found -> (* first time we are asking for a name for that [ip] *)
-      let unique_name = reserve_name_id pid in
-      IndexTbl.add pid unique_name ;
-      unique_name
+    UniquifyPropId.unique_basename pid
 
 end
 
@@ -332,45 +357,27 @@ sig
 end =
 struct
 
-  module NamesTbl = State_builder.Hashtbl(Datatype.String.Hashtbl)(Datatype.Int)
-      (struct
-        let name = "Wp.WpPropId.Names.NamesTbl"
-        let dependencies = [ ]
-        let size = 97
-      end)
-
-  module IndexTbl =
-    State_builder.Hashtbl(Property.Hashtbl)(Datatype.String)
-      (struct
-        let name = "Wp.WpPropId.Names.IndexTbl"
-        let dependencies =
-          [ Ast.self;
-            NamesTbl.self;
-            Globals.Functions.self;
-            Annotations.code_annot_state;
-            Annotations.funspec_state;
-            Annotations.global_state ]
-        let size = 97
-      end)
-
-  let compute_ip ip =
-    let truncate = max 20 (Wp_parameters.TruncPropIdFileName.get ()) in
-    let basename = Property.Names.get_prop_basename ~truncate ip 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 -> (* first time that basename is reserved *)
-      NamesTbl.add basename 2 ; basename
+  (** 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 =
-    try IndexTbl.find ip
-    with Not_found -> (* first time we are asking for a name for that [ip] *)
-      let unique_name = compute_ip ip in
-      IndexTbl.add ip unique_name ;
-      unique_name
+    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
@@ -381,13 +388,22 @@ struct
     | PKVarPos , p -> get_ip p ^ "_positive"
     | PKAFctOut , p -> get_ip p ^ "_normal"
     | PKAFctExit , p -> get_ip p ^ "_exit"
-    | PKPre(_kf,stmt,pre) , _ ->
-        let kf_name_of_stmt =
-          Kernel_function.get_name
-            (Kernel_function.find_englobing_kf stmt)
-        in Printf.sprintf "%s_call_%s" kf_name_of_stmt (get_ip pre)
+    | 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
+        (** remove name of callee kernel function given by get_ip *)
+        let ip_string = get_ip pre in
+        let ip_string =
+          Extlib.opt_conv ip_string
+            (Extlib.string_del_prefix
+               ((Kernel_function.get_name callee_kf)^"_")
+               ip_string)
+        in
+        call_string^"_"^ip_string
 
-  let get_prop_id_name p =
+  let get_prop_id_basename p =
     let basename = get_prop_id_base p in
     match p.p_part with
     | None -> basename
@@ -397,6 +413,14 @@ struct
         if n < 1000 then Printf.sprintf "%s_part%03d" basename (succ k) else
           Printf.sprintf "%s_part%06d" basename (succ k)
 
+  module Uniquify2 = NameUniquify(PropId)(struct
+      let name = "Wp.WpPropId.Names2."
+      let basename = get_prop_id_basename
+    end)
+
+  let get_prop_id_name p =
+    Uniquify2.unique_basename p
+
 end
 
 (* -------------------------------------------------------------------------- *)