From 69f5d8cc1019d2bb8d26f5ad049d20da042841b7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 3 Feb 2021 17:53:25 +0100
Subject: [PATCH] [wp] memoized cfg-infos
---
src/plugins/wp/cfgInfos.ml | 45 ++++++++++++++++++++++++++++++++++++-
src/plugins/wp/cfgInfos.mli | 8 +++----
2 files changed, 48 insertions(+), 5 deletions(-)
diff --git a/src/plugins/wp/cfgInfos.ml b/src/plugins/wp/cfgInfos.ml
index 7dd1486b639..88d853e7117 100644
--- a/src/plugins/wp/cfgInfos.ml
+++ b/src/plugins/wp/cfgInfos.ml
@@ -99,11 +99,39 @@ let collect_calls ~bhv stmt =
x vf args kind loc
| _ -> Fset.empty
+(* -------------------------------------------------------------------------- *)
+(* --- Memoization Key --- *)
+(* -------------------------------------------------------------------------- *)
+
+module Key =
+struct
+ type t = { kf: Kernel_function.t ; bhv : string list ; prop : string list }
+ let compare a b =
+ let cmp = Kernel_function.compare a.kf b.kf in
+ if cmp <> 0 then cmp else
+ let cmp = Stdlib.compare a.bhv b.bhv in
+ if cmp <> 0 then cmp else
+ Stdlib.compare a.prop b.prop
+ let pp_filter kind fmt xs =
+ match xs with
+ | [] -> ()
+ | x::xs ->
+ Format.fprintf fmt "~%s:%s" kind x ;
+ List.iter (Format.fprintf fmt ",%s") xs
+ let pretty fmt k =
+ begin
+ Kernel_function.pretty fmt k.kf ;
+ pp_filter "bhv" fmt k.bhv ;
+ pp_filter "prop" fmt k.prop ;
+ end
+end
+
(* -------------------------------------------------------------------------- *)
(* --- Main Collection Pass --- *)
(* -------------------------------------------------------------------------- *)
-let collect kf cfg ?(bhv=[]) ?(prop=[]) () =
+let compile Key.{ kf ; bhv ; prop } =
+ let cfg = Cfg.get_automaton kf in
let infos = {
cfg ;
annots = false ;
@@ -134,3 +162,18 @@ let collect kf cfg ?(bhv=[]) ?(prop=[]) () =
infos
(* -------------------------------------------------------------------------- *)
+(* --- Memoization Data --- *)
+(* -------------------------------------------------------------------------- *)
+
+module Generator = WpContext.StaticGenerator(Key)
+ (struct
+ type key = Key.t
+ type data = t
+ let name = "Wp.CfgInfos.Generator"
+ let compile = compile
+ end)
+
+let collect kf ?(bhv=[]) ?(prop=[]) () =
+ Generator.get { kf ; bhv ; prop }
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/cfgInfos.mli b/src/plugins/wp/cfgInfos.mli
index a568567c1fc..355a3efcffd 100644
--- a/src/plugins/wp/cfgInfos.mli
+++ b/src/plugins/wp/cfgInfos.mli
@@ -26,10 +26,10 @@ type t
module Cfg = Interpreted_automata
-val collect : Kernel_function.t -> Cfg.automaton ->
- ?bhv:string list ->
- ?prop:string list ->
- unit -> t
+(** Memoized *)
+val collect :
+ Kernel_function.t -> ?bhv:string list -> ?prop:string list -> unit -> t
+
val annots : t -> bool
val doomed : t -> WpPropId.prop_id Bag.t
val calls : t -> Kernel_function.Set.t
--
GitLab