From d607cbe77b4b656ed2722b52a776ef37e042defd Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 17 Sep 2020 13:51:54 +0200
Subject: [PATCH] [wp] Memoisation for hypotheses
---
src/plugins/wp/MemoryContext.ml | 30 +++++++++++++++----
src/plugins/wp/MemoryContext.mli | 14 +++++----
src/plugins/wp/register.ml | 20 ++++++++-----
.../wp/oracle_qualif/wp_call_pre.res.oracle | 4 +--
4 files changed, 48 insertions(+), 20 deletions(-)
diff --git a/src/plugins/wp/MemoryContext.ml b/src/plugins/wp/MemoryContext.ml
index 2904da424d0..b3012f74718 100644
--- a/src/plugins/wp/MemoryContext.ml
+++ b/src/plugins/wp/MemoryContext.ml
@@ -279,10 +279,18 @@ let clauses_of_partition kf loc p =
let reqs = List.sort_uniq Logic_utils.compare_predicate reqs in
reqs
-let emitter =
- Emitter.(create "Wp.Hypotheses" [Funspec] ~correctness:[] ~tuning:[])
-
-let get_behavior kf name partition =
+module Table =
+ State_builder.Hashtbl
+ (Cil_datatype.Kf.Hashtbl)
+ (Datatype.Option(Cil_datatype.Funbehavior))
+ (struct
+ let name = "MemoryContext.Table"
+ let size = 17
+ let dependencies = [ Ast.self ]
+ end)
+
+let compute_behavior kf name hypotheses_computer =
+ let partition = hypotheses_computer kf in
let loc = Kernel_function.get_location kf in
let reqs = clauses_of_partition kf loc partition in
let reqs = List.map Logic_const.new_predicate reqs in
@@ -299,7 +307,17 @@ let get_behavior kf name partition =
b_extended = []
}
-let add_behavior kf name partition =
- match get_behavior kf name partition with
+let compute name hypotheses_computer =
+ Globals.Functions.iter
+ (fun kf -> ignore (compute_behavior kf name hypotheses_computer))
+
+let get_behavior kf name hypotheses_computer =
+ Table.memo (fun kf -> compute_behavior kf name hypotheses_computer) kf
+
+let emitter =
+ Emitter.(create "Wp.Hypotheses" [Funspec] ~correctness:[] ~tuning:[])
+
+let add_behavior kf name hypotheses_computer =
+ match get_behavior kf name hypotheses_computer with
| None -> ()
| Some bhv -> Annotations.add_behaviors emitter kf [bhv]
diff --git a/src/plugins/wp/MemoryContext.mli b/src/plugins/wp/MemoryContext.mli
index 6c406b1aab8..736617995ed 100644
--- a/src/plugins/wp/MemoryContext.mli
+++ b/src/plugins/wp/MemoryContext.mli
@@ -24,12 +24,16 @@ open Cil_types
type param = NotUsed | ByAddr | ByValue | ByShift | ByRef | InContext | InArray
-val pp_param : Format.formatter -> param -> unit
+val pp_param: Format.formatter -> param -> unit
type partition
-val empty : partition
-val set : varinfo -> param -> partition -> partition
+val empty: partition
+val set: varinfo -> param -> partition -> partition
-val add_behavior : kernel_function -> string -> partition -> unit
-val get_behavior : kernel_function -> string -> partition -> behavior option
+val compute: string -> (kernel_function -> partition) -> unit
+
+val add_behavior:
+ kernel_function -> string -> (kernel_function -> partition) -> unit
+val get_behavior:
+ kernel_function -> string -> (kernel_function -> partition) -> behavior option
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index 580ac961046..78dc895d013 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -99,13 +99,18 @@ let wp_print_memory_context kf bhv fmt =
pp_vdecl vkf ;
end
+let wp_compute_memory_context model =
+ let hypotheses_computer = WpContext.compute_hypotheses model in
+ let name = WpContext.MODEL.id model in
+ MemoryContext.compute name hypotheses_computer
+
let wp_warn_memory_context () =
begin
wp_iter_model
begin fun kf m ->
- let partition = WpContext.compute_hypotheses m kf in
+ let hypotheses_computer = WpContext.compute_hypotheses m in
let model = WpContext.MODEL.id m in
- let hyp = MemoryContext.get_behavior kf model partition in
+ let hyp = MemoryContext.get_behavior kf model hypotheses_computer in
match hyp with
| None -> ()
| Some bhv ->
@@ -121,9 +126,9 @@ let wp_insert_memory_context model =
begin
Wp_parameters.iter_fct
begin fun kf ->
- let hyp = WpContext.compute_hypotheses model kf in
+ let hyp_computer = WpContext.compute_hypotheses model in
let model_id = WpContext.MODEL.id model in
- MemoryContext.add_behavior kf model_id hyp
+ MemoryContext.add_behavior kf model_id hyp_computer
end
end
@@ -171,9 +176,9 @@ let do_wp_report () =
end ;
List.iter (WpReport.export stats) reports ;
end ;
- if Wp_parameters.MemoryContext.get () then
- wp_warn_memory_context ()
- end
+ if Wp_parameters.MemoryContext.get () then
+ wp_warn_memory_context ()
+ end
(* ------------------------------------------------------------------------ *)
(* --- Wp Results --- *)
@@ -812,6 +817,7 @@ let cmdline_run () =
WpContext.on_context (computer#model,WpContext.Global)
LogicBuiltins.dump ();
end ;
+ wp_compute_memory_context computer#model ;
if Wp_parameters.CheckModelHypotheses.get () then
wp_insert_memory_context computer#model fct ;
Generator.compute_selection computer ~fct ~bhv ~prop ()
diff --git a/src/plugins/wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle
index 824ee1a6e31..f27ec49d1b7 100644
--- a/src/plugins/wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle
@@ -2,10 +2,10 @@
[kernel] Parsing tests/wp/wp_call_pre.c (with preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
-[kernel] tests/wp/wp_call_pre.c:53: Warning:
- No code nor implicit assigns clause for function g, generating default assigns from the prototype
[kernel] tests/wp/wp_call_pre.c:53: Warning:
No code nor implicit assigns clause for function f, generating default assigns from the prototype
+[kernel] tests/wp/wp_call_pre.c:53: Warning:
+ No code nor implicit assigns clause for function g, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
[wp] 10 goals scheduled
[wp] [Qed] Goal typed_call_g_call_g_requires_qed_ok_Rga : Valid
--
GitLab